fst_ofLex — Mathlib

English

If a is covered by b in Lex(α × β), then their first projections are covered in α.

Русский

Если a покрывает b в Lex(α × β), тогда их первые проекции покрывают в α.

LaTeX

$$$$ a \prec b \Rightarrow a_{1} \prec b_{1}. $$$$

Lean4

theorem _root_.WCovBy.fst_ofLex {a b : α ×ₗ β} (h : a ⩿ b) : (ofLex a).1 ⩿ (ofLex b).1 :=
  ⟨monotone_fst _ _ h.1, fun c hac hcb ↦ h.2 (c := toLex (c, a.2)) (.left _ _ hac) (.left _ _ hcb)⟩

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