instMulLeftMono — Mathlib

English

If f ≤ g are compactly supported maps α → β and h is another such map, then left-multiplication by h is order preserving: h · f ≤ h · g (pointwise).

Русский

Если f ≤ g — компактно поддерживаемые отображения α → β и h — такое же отображение, то умножение слева на h сохраняет порядок: h·f ≤ h·g (поточечно).

LaTeX

$$$$ \forall x \in \alpha,\ f(x) \le g(x) \Rightarrow h(x) f(x) \le h(x) g(x). $$$$

Lean4

instance instMulLeftMono [PartialOrder β] [MulZeroClass β] [ContinuousMul β] [MulLeftMono β] : MulLeftMono C_c(α, β) :=
  ⟨fun _ _ _ hg₁₂ x => mul_le_mul_left' (hg₁₂ x) _⟩

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