Commit 2024-03-27 13:47 59a00afa

View on Github →

chore(Probability/Kernel/CondCdf): cleanup (#10635)

depends on: #10298

Estimated changes

Modified Mathlib/Data/Real/Archimedean.lean

added theorem Real.iInter_Iic_rat

added theorem Real.iUnion_Iic_rat

added theorem Real.not_bddAbove_coe

added theorem Real.not_bddBelow_coe

Modified Mathlib/Probability/Kernel/CondCdf.lean

deleted theorem Real.iInter_Iic_rat

deleted theorem Real.iUnion_Iic_rat