instSMulOrderIso

Mathlib.Algebra.Order.Group.Action.Flag

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

English

The action of an order isomorphism on a flag is defined by applying the isomorphism to the flag's sets: e • s = map e s.

Русский

Действие отношения упорядочения на флаг задаётся отображением множества: e • s = map e s.

LaTeX

$$e \cdot s = map\ e\ s$$

Lean4

instance : SMul (α ≃o α) (Flag α) where smul e := map e

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

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

Разделы

Аффилиация

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