sInf_le

Mathlib.Topology.UniformSpace.Basic

URI: https://scilib.ai/kg/mathlib#UniformSpace.sInf_le

← MathLib Explorer

English

If t is in a family tt of UniformSpaces, then sInf tt ≤ t.

Русский

Если t принадлежит множеству tt униформных пространств, то sInf tt ≤ t.

LaTeX

$$$\text{If } t ∈ tt, \; sInf tt ≤ t$$$

Lean4

protected theorem sInf_le {tt : Set (UniformSpace α)} {t : UniformSpace α} (h : t ∈ tt) : sInf tt ≤ t :=
  show ⨅ u ∈ tt, 𝓤[u] ≤ 𝓤[t] from iInf₂_le t h

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

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

Разделы

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

Аффилиация

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