instSetLike — Mathlib

English

The collection of CompactOpens α forms a set-like structure over α, in particular each element behaves as a subset of α.

Русский

Коллекция CompactOpens α образует множество-подобную структуру над α; каждый элемент ведет себя как подмножество α.

LaTeX

$$$\text{CompactOpens}(α) \text{ carries a set-like structure over } α$$$

Lean4

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

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