uIcc_subset_uIcc_left

Mathlib.Order.Interval.Finset.Basic

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

English

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

Русский

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

LaTeX

$$$\bigl(x \in [[a, b]]\bigr) \Rightarrow [[a, x]] \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