one_le_elim_iff — Mathlib

English

Let β be a type with a compatible order and a distinguished element 1, and let v1 : α1 → β and v2 : α2 → β be two functions. Then the function Sum.elim v1 v2 satisfies 1 ≤ Sum.elim v1 v2 if and only if 1 ≤ v1 and 1 ≤ v2 (pointwise).

Русский

Пусть β — множество с упорядоченным отношением и единицей 1, и пусть v1 : α1 → β и v2 : α2 → β. Тогда функция Sum.elim v1 v2 удовлетворяет 1 ≤ Sum.elim v1 v2 тогда и только тогда, когда 1 ≤ v1 и 1 ≤ v2 (поэлементно).

LaTeX

$$$1 \le \mathrm{Sum\,elim}(v_1,v_2) \iff (1 \le v_1) \wedge (1 \le v_2)$$$

Lean4

@[to_additive]
theorem one_le_elim_iff : 1 ≤ Sum.elim v₁ v₂ ↔ 1 ≤ v₁ ∧ 1 ≤ v₂ :=
  const_le_elim_iff

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