English
Flags are preserved under order isomorphisms; there is an induced map between Flag α and Flag β from an order isomorphism e: α ≃o β.
Русский
Флаги сохраняются под отображениями, сохраняющими порядок; существует отображение между Flag α и Flag β, вызываемое порядка изоморфизмом e.
LaTeX
$$$def\\ map \\, (e : α \\simeq_o β) : Flag α \\simeq Flag β$$$
Lean4
/-- Flags are preserved under order isomorphisms. -/
def map (e : α ≃o β) : Flag α ≃ Flag β
where
toFun s := ofIsMaxChain _ (s.maxChain.image e)
invFun s := ofIsMaxChain _ (s.maxChain.image e.symm)
left_inv s := ext <| e.symm_image_image s
right_inv s := ext <| e.image_symm_image s
