Commit 2025-01-07 19:57 b7ad83b4

View on Github →

feat(LowerUpperTopology): add lemmas (#20465) Add lemmas supporting a future refactor of LowerSemicontinuous.

Estimated changes

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

added theorem Topology.IsLower.tendsto_nhds_iff_lt

added theorem Topology.IsLower.tendsto_nhds_iff_not_le

added theorem Topology.IsUpper.tendsto_nhds_iff_lt

added theorem Topology.IsUpper.tendsto_nhds_iff_not_le

added theorem Topology.WithLower.continuous_toLower

modified theorem Topology.WithLower.isOpen_def

modified theorem Topology.WithLower.isOpen_preimage_ofLower

added theorem Topology.WithLower.ofLower_le_ofLower

added theorem Topology.WithLower.ofLower_lt_ofLower

added theorem Topology.WithLower.toLower_le_toLower

added theorem Topology.WithLower.toLower_lt_toLower

added theorem Topology.WithUpper.continuous_toUpper

added theorem Topology.WithUpper.ofUpper_le_ofUpper

added theorem Topology.WithUpper.ofUpper_lt_ofUpper

added theorem Topology.WithUpper.toUpper_le_toUpper

added theorem Topology.WithUpper.toUpper_lt_toUpper