continuous_Prop — Mathlib

English

Let α be a topological space and p : α → Prop a predicate. Then p is continuous iff the set {x ∈ α : p(x)} is open.

Русский

Пусть α — топологическое пространство и p : α → Prop — предикат. Тогда p непрерывен тогда и только тогда, когда множество {x ∈ α | p(x)} открыто во α.

LaTeX

$$$\\mathrm{Continuous}(p) \\iff \\mathrm{IsOpen}\\left\\{x \\in \\alpha \\mid p(x)\\right\\}$$$

Lean4

theorem continuous_Prop {p : α → Prop} : Continuous p ↔ IsOpen {x | p x} := by
  simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]; rfl

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