Theorems · Theorem · order theory

Real.sInf_smul_of_nonpos

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

Defined in

Mathlib.Data.Real.Pointwise

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingModuleIsOrderedModule