equivSubtype — Mathlib

English

Another natural equivalence between irreducible closed sets and closed irreducible subsets represented as a subtype.

Русский

Еще одно естественное эквивалентное представление между неразложимыми замкнутыми множествами и замкнутыми неразложимыми подмножествами как подтип.

LaTeX

$$$\mathrm{IrreducibleCloseds}(\alpha) \simeq { x : \mathrm{Set}(\alpha) // IsClosed x ∧ IsIrreducible x }$$$

Lean4

/-- The equivalence between `IrreducibleCloseds α` and `{x : Set α // IsIrreducible x ∧ IsClosed x }`.
-/
@[simps apply symm_apply]
def equivSubtype : IrreducibleCloseds α ≃ { x : Set α // IsIrreducible x ∧ IsClosed x }
    where
  toFun a := ⟨a.1, a.2, a.3⟩
  invFun a := ⟨a.1, a.2.1, a.2.2⟩

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