English
For a flag s in a poset α and elements a,b of the flag, the cover relation between a and b after embedding into α coincides with the cover relation in the flag.
Русский
Для флага s в частично упорядоченном множестве α и элементов a,b из флага, отношение покрытия между a и b после вложения в α совпадает с отношением покрытия внутри самого флага.
LaTeX
$$$ (a : \\alpha) \\mathrm{CovBy} b \\;\\iff\\; a \\mathrm{CovBy} b. $$$
Lean4
@[simp, norm_cast]
theorem coe_wcovBy_coe : (a : α) ⩿ b ↔ a ⩿ b :=
by
refine
and_congr_right' ⟨fun h c hac ↦ h hac, fun h c hac hcb ↦ @h ⟨c, mem_iff_forall_le_or_ge.2 fun d hd ↦ ?_⟩ hac hcb⟩
classical
obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
· exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
· exact .inl (hcb.le.trans hbd)
· cases h had hdb
