ofIsClopen — Mathlib

English

From a clopen set A in X, construct a discrete quotient where two points are equivalent iff exactly one of them lies in A.

Русский

Из кликоподножестной части множества A в X строится дискретный фактор-множество, где две точки эквивалентны, если ровно одна из них принадлежит A.

LaTeX

$$$$\text{ofIsClopen}(A) : \text{DiscreteQuotient}(X)$$ with $\; x \sim y \iff (x \in A) \leftrightarrow (y \in A).$$$$

Lean4

/-- Construct a discrete quotient from a clopen set. -/
def ofIsClopen {A : Set X} (h : IsClopen A) : DiscreteQuotient X
    where
  toSetoid := ⟨fun x y => x ∈ A ↔ y ∈ A, fun _ => Iff.rfl, Iff.symm, Iff.trans⟩
  isOpen_setOf_rel x := by by_cases hx : x ∈ A <;> simp [hx, h.1, h.2, ← compl_setOf]

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