Theorem iInf_ulift

Modification history

2026-03-20 14:17

Mathlib/Order/CompleteLattice/Basic.lean

chore: use @[to_dual] extensively in CompleteLattice (#35209) …

Deleted iInf_ulift View on Github →

2024-07-23 12:07

Mathlib/Order/CompleteLattice.lean

refactor: Make `Frame` extend `HeytingAlgebra` (#10560) …

Added iInf_ulift View on Github →