direction_iInf

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#AffineSubspace.direction_iInf

← MathLib Explorer

English

The direction of the infimum over a family is bounded above by the infimum of the directions.

Русский

Направление инфимума над семейством ограничено инфимом направлений.

LaTeX

$$direction (iInf s) ≤ ⨅ i, (s i).direction$$

Lean4

theorem direction_iInf (s : ι → AffineSubspace k P) : (iInf s).direction ≤ ⨅ i, (s i).direction :=
  by
  apply (direction_sInf _).trans_eq
  rw [iInf_range]

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

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

Разделы

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

Аффилиация

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