image2_subset_map₂ — Mathlib

English

Each pair (m,n) with m ∈ p and n ∈ q yields f(m,n) ∈ map₂ f p q; i.e., Set.image2 is contained in map₂.

Русский

Каждая пара (m,n) с m ∈ p и n ∈ q даёт f(m,n) ∈ map₂ f p q; то есть Set.image2 ⊆ map₂.

LaTeX

$$Set.image2 (fun m n => f m n) (↑p : Set M) (↑q : Set N) ⊆ (↑(map₂ f p q) : Set P)$$

Lean4

theorem image2_subset_map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    Set.image2 (fun m n => f m n) (↑p : Set M) (↑q : Set N) ⊆ (↑(map₂ f p q) : Set P) :=
  by
  rintro _ ⟨i, hi, j, hj, rfl⟩
  exact apply_mem_map₂ _ hi hj

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