coe_map

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#Flag.coe_map

English

The carrier of the mapped flag is the image of the original carrier under the order isomorphism.

Русский

Носитель образованного флага равен образу исходного носителя под изоморфизмом порядка.

LaTeX

$$$↑(map e s) = e '' s$$$

Lean4

@[simp, norm_cast]
theorem coe_map (e : α ≃o β) (s : Flag α) : ↑(map e s) = e '' s :=
  rfl

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

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

Разделы

Аффилиация

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