uIcc_subset_uIcc_left

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

If x ∈ [[a, b]], then [[x, b]] ⊆ [[a, b]].

Русский

Если x ∈ [[a, b]], то [[x, b]] ⊆ [[a, b]].

LaTeX

$$$ (x) \\in [[a,b]] \\Rightarrow [[x,b]] \\subseteq [[a,b]] $$$

Lean4

theorem uIcc_subset_uIcc_left (h : x ∈ [[a, b]]) : [[a, x]] ⊆ [[a, b]] :=
  uIcc_subset_uIcc left_mem_uIcc h

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

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

Разделы

Аффилиация

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