equivSubtype' — Mathlib

English

Equivalence between irreducible closed sets and the subtype of closed irreducible subsets (alternate formulation).

Русский

Эквивалентность между неразложимыми замкнутыми множествами и подтипом замкнутых неразложимых подмножеств (альтернативная формулировка).

LaTeX

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

Lean4

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

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