comap_inf

Mathlib.Order.Filter.Map

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

English

The comap distributes over infimum: comap m (g1 ⊓ g2) = comap m g1 ⊓ comap m g2.

Русский

Комап распределяется по снизу: comap m (g1 ⊓ g2) = comap m g1 ⊓ comap m g2.

LaTeX

$$$\\mathrm{comap}\\ m\\ (g_1 \\wedge g_2) = \\mathrm{comap}\\ m\\ g_1 \\wedge \\mathrm{comap}\\ m\\ g_2$$$

Lean4

@[simp]
theorem comap_inf : comap m (g₁ ⊓ g₂) = comap m g₁ ⊓ comap m g₂ :=
  (gc_map_comap m).u_inf

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

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

Разделы

Аффилиация

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