coe_covBy_coe — Mathlib

English

For elements a,b of a flag, the cover relation between their representatives in α is equivalent to the cover relation between the flag representatives.

Русский

Для элементов a,b флага эквивалентно сравнение их представителей в α и отношение покрытия между ними внутри флага.

LaTeX

$$$ (a : \\alpha) \\mathrm{⋖} b \\iff a \\mathrm{⋖} b. $$$

Lean4

@[simp, norm_cast]
theorem coe_covBy_coe : (a : α) ⋖ b ↔ a ⋖ b := by simp [covBy_iff_wcovBy_and_not_le]

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