fst_eq_or_snd_eq_of_wcovBy — Mathlib

English

If x ⩿ y in the product order, then either the first components are equal or the second components are equal.

Русский

Если x ⩿ y в произведении порядков, то либо первые компоненты равны, либо вторые компоненты равны.

LaTeX

$$$ WCovBy(x,y) \Rightarrow x.1 = y.1 \text{ or } x.2 = y.2 $$$

Lean4

theorem fst_eq_or_snd_eq_of_wcovBy : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2 :=
  by
  refine fun h => of_not_not fun hab => ?_
  push_neg at hab
  exact h.2 (mk_lt_mk.2 <| Or.inl ⟨hab.1.lt_of_le h.1.1, le_rfl⟩) (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hab.2.lt_of_le h.1.2⟩)

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