continuous_iff — Mathlib

English

Let B be a topological basis for β. A map f: α → β is continuous if and only if the preimage of every set s in B is open in α.

Русский

Пусть B — топологический базис для β. Тогда отображение f: α → β непрерывно тогда и только тогда, когда предобраз каждого множества s ∈ B открыто в α.

LaTeX

$$$\\mathsf{Continuous}(f) \\iff \\forall s \\in B,\\; \\text{IsOpen}(f^{-1}(s))$$$

Lean4

protected theorem continuous_iff {β : Type*} [TopologicalSpace β] {B : Set (Set β)} (hB : IsTopologicalBasis B)
    {f : α → β} : Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s) := by rw [hB.eq_generateFrom, continuous_generateFrom_iff]

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