rel_add_right — Mathlib

English

Rel r as (bs0 + bs1) iff exists as0 as1 with Rel r as0 bs0 and Rel r as1 bs1 and as = as0 + as1.

Русский

Rel r as (bs0 + bs1) эквивалентно существованию as0, as1 с Rel r as0 bs0 и Rel r as1 bs1 и as = as0 + as1.

LaTeX

$$$$ \forall as, bs_0, bs_1, \text{Rel}(r, as, bs_0+bs_1) \iff \exists as_0, as_1, \text{Rel}(r, as_0, bs_0) \land \text{Rel}(r, as_1, bs_1) \land as = as_0 + as_1 $$$$

Lean4

theorem rel_add_right {as bs₀ bs₁} : Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁ :=
  by rw [← rel_flip, rel_add_left]; simp [rel_flip]

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