coe_iInf₂

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#Interval.coe_iInf₂

← MathLib Explorer

English

For LocallyFiniteOrder α, the Finset Icc a b is nonempty iff a ≤ b.

Русский

Для локально конечного порядка α множество Finset Icc a b непусто тогда, когда a ≤ b.

LaTeX

$$$$ (Icc\\ a\\ b)\\ Nonempty \\iff a \\le b. $$$$

Lean4

@[norm_cast]
theorem coe_iInf₂ [DecidableLE α] (f : ∀ i, κ i → Interval α) : ↑(⨅ (i) (j), f i j) = ⋂ (i) (j), (f i j : Set α) := by
  simp_rw [coe_iInf]

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

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

Разделы

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

Аффилиация

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