frameMinimalAxioms — Mathlib

English

For any open U, U ≠ ⊥ iff the underlying set is nonempty.

Русский

Для любого открытого множества U верно: U ≠ ⊥ тогда и только тогда, когда подмножество непусто.

LaTeX

$$$ U \neq ⊥ \iff (U : Set α) \neq \varnothing $$$

Lean4

/-- Open sets in a topological space form a frame. -/
def frameMinimalAxioms : Frame.MinimalAxioms (Opens α) where
  inf_sSup_le_iSup_inf a s := (ext <| by simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]).le

Похожие утверждения