copy_eq

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.copy_eq

English

If hs expresses s = carrier(L), then the copy equals the original sublattice: L.copy s hs = L.

Русский

Если hs задаёт равенство s и носителя L, то копия равна исходной подрешетке: L.copy s hs = L.

LaTeX

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

Lean4

theorem copy_eq (L : Sublattice α) (s : Set α) (hs) : L.copy s hs = L :=
  SetLike.coe_injective hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru