Commit 2024-01-29 14:47 00b71ef0

View on Github →

refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone (#10046)

Estimated changes

Modified Mathlib/Probability/Kernel/CondCdf.lean

deleted theorem tendsto_of_antitone

Modified Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean

added theorem tendsto_of_antitone