isOpen_iff — Mathlib

English

In a compactly coherent space, a set A is open exactly when for every compact K, the intersection K ∩ A is open in K.

Русский

В компактно-согласованном пространстве множество A открыто тогда и только тогда, когда для каждого компактного подпространства K пересечение K ∩ A является открытым в K.

LaTeX

$$$ \operatorname{IsOpen}(A) \iff \forall K,\, \operatorname{IsCompact}(K) \Rightarrow \operatorname{IsOpen}(K \cap A) $$$$

Lean4

/-- A set `A` in a compactly coherent space is open iff for every compact set `K`, the intersection
`K ∩ A` is open in `K`. -/
theorem isOpen_iff [CompactlyCoherentSpace X] {A : Set X} : IsOpen A ↔ ∀ K, IsCompact K → IsOpen (K ↓∩ A) :=
  IsCoherentWith.isOpen_iff isCoherentWith

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