add_mem_Icc_iff_right — Mathlib

English

For all a,b,c,d in an additive ordered group, a+b ∈ Ico(c,d) iff b ∈ Ico(c−a, d−a).

Русский

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

LaTeX

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

Lean4

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

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