Commit 2023-02-07 04:16 c776695d

View on Github →

feat: port Topology.Order.Lattice (#2129)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Order/Lattice.lean

added theorem Continuous.inf

added theorem Continuous.sup

added theorem Filter.Tendsto.inf_right_nhds'

added theorem Filter.Tendsto.inf_right_nhds

added theorem Filter.Tendsto.sup_right_nhds'

added theorem Filter.Tendsto.sup_right_nhds

added theorem continuous_inf

added theorem continuous_sup