iInf_mem

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.iInf_mem

English

Let f : ι → X. If every f(i) belongs to S, then the infimum of {f(i) | i ∈ ι} belongs to S.

Русский

Пусть f : ι → X. Тогда если для всех i выполняется f(i) ∈ S, то ⨅ i, f(i) ∈ S.

LaTeX

$$$( \forall i, f(i) \in S) \Rightarrow \operatorname{iInf}_i f(i) \in S$$$

Lean4

theorem iInf_mem (hf : ∀ i, f i ∈ S) : ⨅ i, f i ∈ S :=
  S.sInf_mem <| by simpa [range_subset_iff]

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

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

Разделы

Аффилиация

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