mapsTo_union — Mathlib

English

MapsTo f (s1 ∪ s2) t holds exactly when both MapsTo f s1 t and MapsTo f s2 t hold.

Русский

Отображение f на s1 ∪ s2 попадает в t тогда и только тогда, когда f отображает s1 в t и отображает s2 в t.

LaTeX

$$$\\\\MapsTo f (s_1 \\\\cup s_2) t \\\\leftrightarrow (\\\\MapsTo f s_1 t \\\\land \\\\MapsTo f s_2 t)$$$

Lean4

@[simp]
theorem mapsTo_union : MapsTo f (s₁ ∪ s₂) t ↔ MapsTo f s₁ t ∧ MapsTo f s₂ t :=
  ⟨fun h => ⟨h.mono subset_union_left (Subset.refl t), h.mono subset_union_right (Subset.refl t)⟩, fun h =>
    h.1.union h.2⟩

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