setOf_isOpen — Mathlib

English

The set of open sets in X equals the image under preimage f of the open sets in Y.

Русский

Множество открытых в X равно образу через прообраз F открытых множеств в Y.

LaTeX

$$$\{s : \ Set X \mid \operatorname{IsOpen}(s)\} = \operatorname{image} (\operatorname{preimage}(f))^{\; }\{t : \Set Y \mid \operatorname{IsOpen}(t)\}.$$$

Lean4

theorem setOf_isOpen (hf : IsInducing f) : {s : Set X | IsOpen s} = preimage f '' {t | IsOpen t} :=
  Set.ext fun _ ↦ hf.isOpen_iff

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