of_continuous_prop — Mathlib

English

If a universal property h says that whenever a function is pointwise continuous on every member of S then it is continuous on X, then S is coherent.

Русский

Если существует универсальное свойство h, гласящее: если f непрерывна на каждом s∈S, то она непрерывна на X, тогда S когерентно.

LaTeX

$$$ \\big( \\forall f: X \\to \\text{Prop}, (\\forall s \\in S, \\text{ContinuousOn}(f, s)) \\to \\text{Continuous}(f) \\big) \\to \\text{IsCoherentWith} S $$$

Lean4

theorem of_continuous_prop (h : ∀ f : X → Prop, (∀ s ∈ S, ContinuousOn f s) → Continuous f) : IsCoherentWith S where
  isOpen_of_forall_induced u
    hu := by
    simp only [continuousOn_iff_continuous_restrict, continuous_Prop] at *
    exact h _ hu

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