mapsTo_inter — Mathlib

English

MapsTo f s (t1 ∩ t2) is equivalent to MapsTo f s t1 and MapsTo f s t2.

Русский

Отображение f на s попадает в t1 ∩ t2 тогда и только тогда, когда оно попадает в t1 и в t2.

LaTeX

$$$\\\\MapsTo f s (t_1 \\\\cap t_2) \\\\leftrightarrow (\\\\MapsTo f s t_1 \\\\land \\\\MapsTo f s t_2)$$$

Lean4

@[simp]
theorem mapsTo_inter : MapsTo f s (t₁ ∩ t₂) ↔ MapsTo f s t₁ ∧ MapsTo f s t₂ :=
  ⟨fun h => ⟨h.mono (Subset.refl s) inter_subset_left, h.mono (Subset.refl s) inter_subset_right⟩, fun h =>
    h.1.inter h.2⟩

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