add_mem_Ico_iff_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_mem_Ico_iff_left : a + b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c - b) (d - b) :=
  (and_congr sub_le_iff_le_add lt_sub_iff_add_lt).symm

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