elim_le_elim_iff — Mathlib

English

Let β be a type with a preorder and α1, α2 be index types. For u1,u2,v1,v2 : α1→β, α2→β, the order of the combined function Sum.elim u1 u2 is equivalent to the pair of orders u1 ≤ v1 and u2 ≤ v2.

Русский

Пусть β имеет предзаказ, а α1, α2 — индексовые типы. Для функций u1,u2: α1→β и v1,v2: α2→β, порядок Sum.elim u1 u2 ≤ Sum.elim v1 v2 равносилен u1 ≤ v1 и u2 ≤ v2.

LaTeX

$$$\text{Sum.elim } u_1 u_2 \le \text{Sum.elim } v_1 v_2 \iff u_1 \le v_1 \land u_2 \le v_2$$$

Lean4

@[simp]
theorem elim_le_elim_iff {u₁ v₁ : α₁ → β} {u₂ v₂ : α₂ → β} : Sum.elim u₁ u₂ ≤ Sum.elim v₁ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂ :=
  Sum.forall

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