Theorem lowerClosure_sUnion

Modification history

2026-03-23 08:24

Mathlib/Order/UpperLower/Closure.lean

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

Deleted lowerClosure_sUnion View on Github →

2025-03-24 10:45

Mathlib/Order/UpperLower/Basic.lean

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

Modified lowerClosure_sUnion View on Github →

2023-05-14 07:05

Mathlib/Order/UpperLower/Basic.lean

chore: Rename to `sSup`/`iSup` (#3938) …

Added lowerClosure_sUnion View on Github →