Ultrafilter-Measure Lean formalization
Formalization of the measure representation of ultrafilters: the measure defined by an ultrafilter and the ultrafilter defined by a measure.
HTML-rendered Lean proofs:
Defs.lean
Measure_to_ultrafilter.lean
Ultrafilter_to_measure.lean