Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-02-21 15:30
02dc6f25
View on Github →
feat(probability/stopping): filtrations are a complete lattice (
#12169
)
Estimated changes
Modified
src/probability/stopping.lean
deleted
def
measure_theory.const_filtration
added
theorem
measure_theory.filtration.Inf_def
added
theorem
measure_theory.filtration.Sup_def
added
theorem
measure_theory.filtration.coe_fn_inf
added
theorem
measure_theory.filtration.coe_fn_sup
added
def
measure_theory.filtration.const