instSetLike — Mathlib

English

The family of subcomplexes of a RelCWComplex C forms a SetLike structure, where the coercion to X is E.carrier and is injective up to equality of carriers.

Русский

Множество подкомплексoв RelCWComplex C образует структуру SetLike: привод к X есть E.carrier и эта карта инъективна по носителю.

LaTeX

$$$$\text{instance: } SetLike(\text{Subcomplex } C) X\text{ with } (E \mapsto E.carrier) \text{ and } (E,F)\mapsto \text{equality constraints}$$$$

Lean4

instance : SetLike (Subcomplex C) X where
  coe E := E.carrier
  coe_injective' E F
    h := by
    obtain ⟨E, _, _, hE⟩ := E
    obtain ⟨F, _, _, hF⟩ := F
    congr
    apply eq_of_eq_union_iUnion
    rw [hE, hF]
    simpa using h

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