isOpen_induced_iff — Mathlib

English

A set s is open in the induced topology t.induced f on α iff there exists an open t-set whose preimage under f is s.

Русский

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

LaTeX

$$$IsOpen[t.induced f]\, s \\iff \\exists t, IsOpen t \\wedge f^{-1}(t) = s$$$

Lean4

theorem isOpen_induced_iff [t : TopologicalSpace β] {s : Set α} {f : α → β} :
    IsOpen[t.induced f] s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s :=
  Iff.rfl

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