prod_le_prod_iff — Mathlib

English

Characterizes when s1 ×ˢ t1 ≤ s2 ×ˢ t2: this holds iff either s1 ≤ s2 and t1 ≤ t2, or s2 = ⊤ or t2 = ⊤.

Русский

Характеризуется, когда s1 ×ˢ t1 ≤ s2 ×ˢ t2: выполняется либо s1 ≤ s2 и t1 ≤ t2, либо s2 = ⊤ или t2 = ⊤.

LaTeX

$$$ s_1 \times^{\mathrm{S}} t_1 \le s_2 \times^{\mathrm{S}} t_2 \iff \bigl((s_1 \le s_2) \wedge (t_1 \le t_2)\bigr) \lor (s_2 = \top) \lor (t_2 = \top) $$$$

Lean4

theorem prod_le_prod_iff : s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤ :=
  prod_subset_prod_iff.trans <| by simp

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