coe_copy — Mathlib

English

If you copy a complete sublattice along an equality of carriers, the result has the same carrier as the given set, i.e., the copy is definitional to the carrier s.

Русский

Если выполнить копирование полной подподрешетки вдоль равенства носителей, то полученная копия имеет тот же носитель, что и заданное множество s.

LaTeX

$$$L.copy\,s\,hs = s$$$

Lean4

@[simp, norm_cast]
theorem coe_copy (s : Set α) (hs) : L.copy s hs = s :=
  rfl

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