coe_copy — Mathlib

English

The coercion from a copied subalgebra equals the original carrier; i.e., if hs expresses that s equals L, then L.copy s hs coerces to s.

Русский

Переход через копирование подпалгебры к базовому представлению равен исходному множеству, если hs доказывает равенство s и L.

LaTeX

$$$L.copy s hs = s$$$

Lean4

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

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