le_smul_iff — Mathlib

English

The left/right subword is characterized by a condition: h ≤ f • g if and only if for all s ∈ f and t ∈ g, the product s • t ∈ h.

Русский

Левая часть условного равенства характеризуется: h ≤ f • g тогда и только тогда, когда для всех s ∈ f и t ∈ g, s • t ∈ h.

LaTeX

$$$h \le f \cdot g \iff \forall \{s\}, s \in f \to \forall \{t\}, t \in g \to s \cdot t \in h$$$

Lean4

@[to_additive (attr := simp)]
theorem le_smul_iff : h ≤ f • g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s • t ∈ h :=
  le_map₂_iff

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