isOpen_iff — Mathlib

English

If S is a coherent family of subsets of X, then a set t is open in X if and only if its preimage under the inclusion map to every S ∈ S is open in S.

Русский

Пусть S — когерентное семейство подмножеств X. Тогда множество t открыто в X тогда и только тогда, когда его прообраз под включающим отображением в любую s ∈ S открыто в s.

LaTeX

$$$ IsOpen\\,t \\iff \\forall s \\in S, IsOpen\\left((\\uparrow)^{-1}' t : Set\\, s\\right) $$$

Lean4

protected theorem isOpen_iff (hS : IsCoherentWith S) : IsOpen t ↔ ∀ s ∈ S, IsOpen ((↑) ⁻¹' t : Set s) :=
  ⟨fun ht _ _ ↦ ht.preimage continuous_subtype_val, hS.1 t⟩

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