map_inl_disjUnion_map_inr — Mathlib

English

The disjoint union built from left- and right-injected maps satisfies a definitional equality: the disjoint union of s mapped by inl and t mapped by inr is exactly the disjoint sum s.disjSum t.

Русский

Дизъюнктивное объединение, построенное из отображений влево и вправо, удовлетворяет определённому равенству: левая карта из s и правая карта из t образуют ровно дизъюнктивную сумму s.disjSum t.

LaTeX

$$$(s\mapsto \mathrm{inl})\,s \disjUnion (t\mapsto \mathrm{inr})\,t = s\disjSum t$$$

Lean4

@[simp]
theorem map_inl_disjUnion_map_inr :
    (s.map Embedding.inl).disjUnion (t.map Embedding.inr) (disjoint_map_inl_map_inr _ _) = s.disjSum t :=
  rfl

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