inter_inter — Mathlib

English

If f maps s1 to t1 and f maps s2 to t2, then f maps s1 ∩ s2 to t1 ∩ t2.

Русский

Если f отображает s1 в t1 и s2 в t2, то f отображает s1 ∩ s2 в t1 ∩ t2.

LaTeX

$$$\\\\MapsTo f s_1 t_1 \\\\land \\\\MapsTo f s_2 t_2 \\\\rightarrow \\\\MapsTo f (s_1 \\\\cap s_2) (t_1 \\\\cap t_2)$$$

Lean4

theorem inter_inter (h₁ : MapsTo f s₁ t₁) (h₂ : MapsTo f s₂ t₂) : MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂) := fun _ hx =>
  ⟨h₁ hx.1, h₂ hx.2⟩

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