IicExtend

Mathlib.Order.Interval.Set.ProjIcc

URI: https://scilib.ai/kg/mathlib#Set.OrdConnected.IicExtend

← MathLib Explorer

English

For x in the core of Iic b, IicExtend f x equals f x.

Русский

Для x в ядре Iic b IicExtend f x равно f x.

LaTeX

$$$(\\mathrm{IicExtend} f)(x) = f x$ для x ∈ (\\mathrm{Iic} b).\\mathrm{Elem}$$

Lean4

protected theorem IicExtend {s : Set (Iic b)} (hs : s.OrdConnected) : {x | IicExtend (· ∈ s) x}.OrdConnected :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨min_le_min le_rfl hz.1, min_le_min le_rfl hz.2⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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