copy — Mathlib

English

For E ∈ Subcomplex C, the underlying set ↑E is contained in C.

Русский

Для E ∈ Subcomplex C носитель E содержится в C.

LaTeX

$$$$\uparrow E \subseteq C$$$$

Lean4

/-- Copy of a `Subcomplex` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) :
    Subcomplex C :=
  { carrier := F
    I := J
    closed' := hF.symm ▸ E.closed'
    union' := hF.symm ▸ hJ ▸ E.union' }

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