map₂_le — Mathlib

English

A submodule map₂ f p q is contained in r if and only if every bilinear image of elements from p and q lies in r.

Русский

Подмодуль map₂ f p q содержится в r тогда и только тогда, когда каждое изображение вида f(m,n) с m∈p, n∈q принадлежит r.

LaTeX

$$map₂ f p q ≤ r ↔ ∀ m ∈ p, ∀ n ∈ q, f m n ∈ r$$

Lean4

theorem map₂_le {f : M →ₗ[R] N →ₗ[R] P} {p : Submodule R M} {q : Submodule R N} {r : Submodule R P} :
    map₂ f p q ≤ r ↔ ∀ m ∈ p, ∀ n ∈ q, f m n ∈ r :=
  ⟨fun H _m hm _n hn => H <| apply_mem_map₂ _ hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

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