Commit 2023-10-25 14:17 65b7d164
View on Github →feat: generalize some lemmas to directed types (#7852)
New lemmas / instances
- An archimedean ordered semiring is directed upwards.
Filter.hasAntitoneBasis_atTop
;Filter.HasAntitoneBasis.iInf_principal
;
Fix typos
- Docstrings: "if the agree" -> "if they agree".
ProbabilityTheory.measure_eq_zero_or_one_of_indepSetCat_self
->ProbabilityTheory.measure_eq_zero_or_one_of_indepSet_self
.
Weaken typeclass assumptions
From a semilattice to a directed type
MeasureTheory.tendsto_measure_iUnion
;MeasureTheory.tendsto_measure_iInter
;Monotone.directed_le
,Monotone.directed_ge
;Antitone.directed_le
,Antitone.directed_ge
;directed_of_sup
, renamed todirected_of_isDirected_le
;directed_of_inf
, renamed todirected_of_isDirected_ge
;
From a strict ordered semiring to an ordered semiring
tendsto_nat_cast_atTop_atTop
;Filter.Eventually.nat_cast_atTop
;atTop_hasAntitoneBasis_of_archimedean
;