map_comap_inl_sup_map_comap_inr

Mathlib.Order.Filter.Map

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

← MathLib Explorer

English

The comap inr of map inl f along the sum type is bottom.

Русский

Комап по inr к образу через inl через сумму равен нулю.

LaTeX

$$$\operatorname{comap} \operatorname{inr} (\operatorname{map} \operatorname{inl} f) = \bot$$$

Lean4

theorem map_comap_inl_sup_map_comap_inr (l : Filter (α ⊕ β)) : map inl (comap inl l) ⊔ map inr (comap inr l) = l := by
  rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]

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

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

Разделы

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

Аффилиация

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