English
The order on the product is given by lt_iff: x < y iff (x1 < y1 ∧ x2 ≤ y2) ∨ (x1 ≤ y1 ∧ x2 < y2).
Русский
Порядок на произведении задаётся выражением lt_iff: x < y, если (x1 < y1 и x2 ≤ y2) или (x1 ≤ y1 и x2 < y2).
LaTeX
$$$x < y \iff \big( x_1 < y_1 \land x_2 \le y_2 \big) \lor \big( x_1 \le y_1 \land x_2 < y_2 \big)$$$
Lean4
theorem lt_iff : x < y ↔ x.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2 :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· by_cases h₁ : y.1 ≤ x.1
· exact Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
· exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩
· rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
· exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩
· exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩
