isLowerSet_of_isOpen — Mathlib

English

Every set open in the lower topology is a lower set.

Русский

Любое открытое в нижней топологии множество является нижним множеством.

LaTeX

$$$\\text{If } s\\text{ is open in the lower topology, then } s \\text{ is a lower set.}$$$

Lean4

/-- Every set open in the lower topology is a lower set. -/
theorem isLowerSet_of_isOpen (h : IsOpen s) : IsLowerSet s :=
  by
  replace h := isOpen_iff_generate_Ici_compl.1 h
  induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih

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