add_mem_Icc_iff_left — Mathlib

English

For any a,b,c,d in a additive ordered group, a+b ∈ Icc(c,d) iff a ∈ Icc(c−b, d−b).

Русский

В аддитивной упорядоченной группе: a+b ∈ Icc(c,d) тогда и только тогда, когда a ∈ Icc(c−b, d−b).

LaTeX

$$$a+b \in \mathrm{Icc}(c,d) \iff a \in \mathrm{Icc}(c-b, d-b)$$$

Lean4

theorem add_mem_Icc_iff_left : a + b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c - b) (d - b) :=
  (and_congr sub_le_iff_le_add le_sub_iff_add_le).symm

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