Commit 2024-02-14 10:22 ed633828

View on Github →

refactor(Probability/Kernel/CondCdf): mv atBot_le_nhds_bot/top (#10132)

Estimated changes

Modified Mathlib/Probability/Kernel/CondCdf.lean

deleted theorem atBot_le_nhds_bot

deleted theorem atTop_le_nhds_top

Modified Mathlib/Topology/Order/Basic.lean

added theorem atBot_le_nhds_bot

added theorem atTop_le_nhds_top