instIsUpperProp — Mathlib

English

The Sierpiński topology on Prop is the upper topology.

Русский

Топология Сьерпински на Prop есть верхняя топология.

LaTeX

$$$\text{IsUpper Prop}$$$

Lean4

/-- The Sierpiński topology on `Prop` is the upper topology -/
instance : IsUpper Prop where
  topology_eq_upperTopology :=
    by
    rw [Topology.upper, sierpinskiSpace, ← generateFrom_insert_empty]
    congr
    exact
      le_antisymm
        (fun h hs => by
          simp only [compl_Iic, mem_setOf_eq]
          rw [← Ioi_True, ← Ioi_False] at hs
          rcases hs with (rfl | rfl)
          · use True
          · use False)
        (by rintro _ ⟨a, rfl⟩; by_cases a <;> aesop (add simp [Ioi, lt_iff_le_not_ge]))

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