elim_le_const_iff — Mathlib

English

Let b be an element of β. The order Sum.elim u1 u2 ≤ const b is equivalent to u1 ≤ const b and u2 ≤ const b.

Русский

Пусть b ∈ β. Порядок Sum.elim u1 u2 ≤ const b эквивалентен u1 ≤ const b и u2 ≤ const b.

LaTeX

$$$\text{Sum.elim } u_1 u_2 \le \text{Function.const } b \iff u_1 \le \text{Function.const } b \land u_2 \le \text{Function.const } b$$$

Lean4

theorem elim_le_const_iff {b : β} {u₁ : α₁ → β} {u₂ : α₂ → β} :
    Sum.elim u₁ u₂ ≤ Function.const _ b ↔ u₁ ≤ Function.const _ b ∧ u₂ ≤ Function.const _ b :=
  elim_const_const b ▸ elim_le_elim_iff ..

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