instMax

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.instMax

English

NonemptyInterval carries a SetLike structure with carrier Icc(s.fst,s.snd).

Русский

NonemptyInterval обладает структурой SetLike с носителем Icc(s.fst,s.snd).

LaTeX

$$$\text{setLike}(s) = \mathrm{Icc}(s.fst,s.snd)$$$

Lean4

instance : Max (NonemptyInterval α) :=
  ⟨fun s t => ⟨⟨s.fst ⊓ t.fst, s.snd ⊔ t.snd⟩, inf_le_left.trans <| s.fst_le_snd.trans le_sup_left⟩⟩

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

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

Разделы

Аффилиация

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