map_sumElim_eq — Mathlib

English

For l on Sum α β and maps m₁, m₂ to γ, the map of Sum.elim equals the supremum of maps after comaps.

Русский

Для l над Sum α β и отображений m₁, m₂ к γ отображение Sum.elim через l равняется наибольшему из отображений после comap.

LaTeX

$$map (Sum.elim m₁ m₂) l = max (map m₁ (comap inl l)) (map m₂ (comap inr l))$$

Lean4

theorem map_sumElim_eq (l : Filter (α ⊕ β)) (m₁ : α → γ) (m₂ : β → γ) :
    map (Sum.elim m₁ m₂) l = map m₁ (comap inl l) ⊔ map m₂ (comap inr l) :=
  by
  rw [← map_comap_inl_sup_map_comap_inr l]
  simp [map_sup, map_map, comap_sup, (gc_map_comap _).u_l_u_eq_u]

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