comap_iInf

Mathlib.Algebra.Group.Subsemigroup.Operations

URI: https://scilib.ai/kg/mathlib#Subsemigroup.comap_iInf

← MathLib Explorer

English

For a family {S_i}, the comap of their infimum equals the infimum of the comaps: (iInf s).comap f = iInf (S).

Русский

Комап инфимума равен инфимуму комап: (iInf s).comap f = iInf s.

LaTeX

$$(iInf s).comap f = iInf (fun i => s i).comap f$$

Lean4

@[to_additive]
theorem comap_iInf {ι : Sort*} (f : M →ₙ* N) (s : ι → Subsemigroup N) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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

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

Разделы

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

Аффилиация

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