eq_biInf

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.HasBasis.eq_biInf

English

If l has basis p s, then l equals the infimum over i of 𝓟(s i) with potential p-bounded index calculus: l = ⨅ i, 𝓟(s i).

Русский

Пусть фильтр l имеет базис p s; тогда l равен инфимума по i от 𝓟(s(i)).

LaTeX

$$$ l = \iInf i, 𝓟(s(i)) $$$

Lean4

theorem eq_biInf (h : l.HasBasis p s) : l = ⨅ (i) (_ : p i), 𝓟 (s i) :=
  eq_biInf_of_mem_iff_exists_mem fun {_} => by simp only [h.mem_iff, mem_principal]

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

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

Разделы

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

Аффилиация

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