Theorems · Theorem · order theory

Set.image_const_add_Ioi

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

Defined in: Mathlib.Algebra.Order.Interval.Set.Monoid
Cited by: 0 results in Mathlib
Foundations: Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid PartialOrder IsOrderedCancelAddMonoid ExistsAddOfLE

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
AddCommMonoidstatement and proof · cited by 12,281
PartialOrderstatement and proof · cited by 6,410
Set.imagestatement · cited by 5,609
add_commproof · cited by 1,535
Set.Ioistatement and proof · cited by 1,463
Set.image_congrproof · cited by 533
IsOrderedCancelAddMonoidstatement and proof · cited by 359
ExistsAddOfLEstatement and proof · cited by 330
Set.image_add_const_Ioiproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.