comap_inf

Mathlib.Algebra.Group.Subsemigroup.Operations

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

English

The comap of the infimum is the infimum of comaps: (S ⊓ T).comap f = S.comap f ⊓ T.comap f.

Русский

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

LaTeX

$$(S ⊓ T).comap f = S.comap f ⊓ T.comap f$$

Lean4

@[to_additive]
theorem comap_inf (S T : Subsemigroup N) (f : M →ₙ* N) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f :=
  (gc_map_comap f).u_inf

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

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

Разделы

Аффилиация

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