isOpen_induced_eq — Mathlib

English

A set s is open in the induced topology on α if and only if s belongs to the image under preimage of f of the set of open sets in α.

Русский

Множество s открыто в индуцированной топологии на α тогда и только тогда, когда оно принадлежит образу подмножества открытых множества в α через f.

LaTeX

$$$\\text{IsOpen}[\\operatorname{induced} f t] s \\iff s \\in (\\operatorname{preimage} f)''\\{ s \\mid \\text{IsOpen } s\\}.$$$

Lean4

theorem isOpen_induced_eq {s : Set α} : IsOpen[induced f t] s ↔ s ∈ preimage f '' {s | IsOpen s} :=
  Iff.rfl

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