left_distrib_of_nonneg_of_ne_top — Mathlib

English

Let x ∈ EReal satisfy x ≥ 0 and x ≠ ⊤, and let y, z ∈ EReal. Then x · (y + z) = x · y + x · z.

Русский

Пусть x ∈ EReal так что x ≥ 0 и x ≠ ⊤, и пусть y, z ∈ EReal. Тогда x · (y + z) = x · y + x · z.

LaTeX

$$$\forall x,y,z \in \mathrm{EReal},\; 0 \le x \land x \ne \top \Rightarrow x(y+z) = xy + xz$$$

Lean4

theorem left_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) :
    x * (y + z) = x * y + x * z := by
  cases hx_nonneg.eq_or_lt' with
  | inl hx0 => simp [hx0]
  | inr hx0 =>
    lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
    cases y <;> cases z <;> simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul]; rw_mod_cast [mul_add]

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