mem_codiscrete' — Mathlib

English

Equivalent formulation of codiscrete membership in terms of open and discrete complement subspace.

Русский

Эквивалентная формулировка принадлежности codiscrete через открытость и дискретную комплементу.

LaTeX

$$$S \in codiscrete X \iff \mathrm{IsOpen}(S) \wedge \text{DiscreteTopology}(S^c).$$$

Lean4

theorem mem_codiscrete' {S : Set X} : S ∈ codiscrete X ↔ IsOpen S ∧ DiscreteTopology ↑Sᶜ := by
  rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]

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