comap_lift_eq

Mathlib.Order.Filter.Lift

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

English

Comap distributes over lift: comap m (f.lift g) = f.lift (comap m ∘ g).

Русский

Комап распределяется над подъемом: comap m (f.lift g) = f.lift (comap m ∘ g).

LaTeX

$$comap m (f.lift g) = f.lift (comap m \circ g)$$

Lean4

theorem comap_lift_eq {m : γ → β} : comap m (f.lift g) = f.lift (comap m ∘ g) := by simp only [Filter.lift, comap_iInf];
  rfl

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

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

Разделы

Аффилиация

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