Theorems · Theorem · order theory

Set.image_affine_Ioc

∀ {K : Type u_2} [inst : DivisionSemiring K] [inst_1 : PartialOrder K] [PosMulReflectLT K] [IsOrderedCancelAddMonoid K]
  [ExistsAddOfLE K] {a : K},
  0 < a → ∀ (b c d : K), (fun x => a * x + b) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)

Defined in

Mathlib.Algebra.Order.Group.Pointwise.Interval

Cited by

2 results in Mathlib

Foundations

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

Assumes

DivisionSemiringPartialOrderPosMulReflectLTIsOrderedCancelAddMonoidExistsAddOfLE