sub_mem_Icc_iff_left — Mathlib

English

Let a,b,c,d ∈ α with α an ordered additive group. The left translation by b moves endpoints of Icc: a − b ∈ Icc(c,d) iff a ∈ Icc(c + b, d + b).

Русский

Пусть a,b,c,d ∈ α, где α — упорядоченная аддитивная группа. Сдвиг слева на b переносит концы Icc: 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 sub_mem_Icc_iff_left : a - b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c + b) (d + b) :=
  and_congr le_sub_iff_add_le sub_le_iff_le_add

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