Theorem lowerClosure_eq

Modification history

2026-03-23 08:24

Mathlib/Order/UpperLower/Closure.lean

chore(Order/UpperLower/Closure): use `to_dual` (#36969) …

Deleted lowerClosure_eq View on Github →

2025-03-24 10:45

Mathlib/Order/UpperLower/Basic.lean

chore: split `Order.UpperLower.Basic` (#23248) …

Modified lowerClosure_eq View on Github →

2024-07-03 09:27

Mathlib/Order/UpperLower/Basic.lean

feat(Topology/Inseparable): Define `specializing` maps between topological spaces (#14001) …

Added lowerClosure_eq View on Github →