Theorems · Theorem · order theory

Real.sInf_smul_of_nonneg

∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : MulActionWithZero α ℝ]
  [IsOrderedModule α ℝ] {a : α}, 0 ≤ a → ∀ (s : Set ℝ), sInf (a • s) = a • sInf s

Defined in

Mathlib.Data.Real.Pointwise

Cited by

3 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingMulActionWithZeroIsOrderedModule