smul_le — Mathlib

English

For AddSubmonoid M of R and N, P of A, M • N ≤ P if and only if for all m ∈ M and n ∈ N, m • n ∈ P.

Русский

Для аддитивного подпорожденного M ⊆ R и N, P ⊆ A верно M • N ≤ P тогда и только тогда, когда для всех m ∈ M и n ∈ N выполняется m • n ∈ P.

LaTeX

$$$M \cdot N \le P \iff \forall m \in M, \forall n \in N, m \cdot n \in P$$$

Lean4

theorem smul_le : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P :=
  ⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

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