copy_eq

Mathlib.Order.CompleteSublattice

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

English

If L.copy s hs copies along the same carrier, then L.copy s hs equals L.

Русский

Если копирование вдоль одного и того же носителя приводит к копии, то L.copy s hs совпадает с L.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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