disjointed_of_isMin

Mathlib.Order.Disjointed

URI: https://scilib.ai/kg/mathlib#disjointed_of_isMin

← MathLib Explorer

English

If i is a minimal element, then disjointed f i equals f i.

Русский

Если i минимален, то disjointed f i = f i.

LaTeX

$$$\forall f,i\;\big( IsMin(i) \Rightarrow disjointed f i = f i \big)$.$$

Lean4

theorem disjointed_of_isMin (f : ι → α) {i : ι} (hn : IsMin i) : disjointed f i = f i :=
  by
  have : Iio i = ∅ := by rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]
  simp only [disjointed_apply, this, sup_empty, sdiff_bot]

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

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

Разделы

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

Аффилиация

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