eq_iInf

Mathlib.Order.Filter.Bases.Basic

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

English

If l has a basis with True as the index predicate, then l is the infimum of principal filters of s i: l = ⨅ i, 𝓟(s i).

Русский

Если у фильтра l имеется базис с истинностью по индексу, то l равен инфимума по i of 𝓟(s(i)).

LaTeX

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

Lean4

theorem eq_iInf (h : l.HasBasis (fun _ => True) s) : l = ⨅ i, 𝓟 (s i) := by simpa only [iInf_true] using h.eq_biInf

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

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

Разделы

Аффилиация

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