Theorems · Theorem · order theory

Set.image_add_const_Icc

∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => x + a) '' Set.Icc b c = Set.Icc (b + a) (c + a)

Defined in

Mathlib.Algebra.Order.Interval.Set.Monoid

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderIsOrderedCancelAddMonoidExistsAddOfLE