const_le_elim_iff — Mathlib

English

Let b be an element of β and u1,u2 be maps into β. Then Sum.elim u1 u2 ≤ const b is equivalent to u1 ≤ const b and u2 ≤ const b.

Русский

Пусть b ∈ β и u1, u2 — отображения в β. Тогда 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 \;\Longleftrightarrow\; u_1 \le \text{Function.const } b \land u_2 \le \text{Function.const } b$$$

Lean4

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

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