sub_mem_Icc_zero_iff_right

Mathlib.Algebra.Order.Interval.Set.Group

URI: https://scilib.ai/kg/mathlib#Set.sub_mem_Icc_zero_iff_right

English

Corollary: b − a ∈ Icc 0 b iff a ∈ Icc 0 b.

Русский

Следствие: b − a ∈ Icc(0,b) тогда и только тогда a ∈ Icc(0,b).

LaTeX

$$$b - a \in \mathrm{Icc}(0, b) \iff a \in \mathrm{Icc}(0, b)$$$

Lean4

theorem sub_mem_Icc_zero_iff_right : b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b := by
  simp only [sub_mem_Icc_iff_right, sub_self, sub_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru