instSetLike — Mathlib

English

There is a canonical SetLike structure making PositiveCompacts α behave as sets of α via their carrier.

Русский

Существует каноническая структура SetLike, делающая PositiveCompacts α формально множествами α через их носитель.

LaTeX

$$$ \text{SetLike}(\text{PositiveCompacts } \alpha) \text{ via } s \mapsto s.\text{carrier}$$$

Lean4

instance : SetLike (PositiveCompacts α) α where
  coe s := s.carrier
  coe_injective' s t
    h := by
    obtain ⟨⟨_, _⟩, _⟩ := s
    obtain ⟨⟨_, _⟩, _⟩ := t
    congr

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