Theorems · Theorem · order theory

Set.uIcc_injective_right

∀ {α : Type u_1} [inst : DistribLattice α] (a : α), Function.Injective fun b => Set.uIcc b a

Defined in: Mathlib.Order.Interval.Set.UnorderedInterval
Cited by: 1 results in Mathlib
Foundations: Depth 13 from the axioms · uses propext, Quot.sound
Assumes: DistribLattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

Setstatement · cited by 53,352
Set.uIccstatement and proof · cited by 393
DistribLatticestatement and proof · cited by 150
Set.ext_iffproof · cited by 90
Set.left_mem_uIccproof · cited by 17
Set.eq_of_mem_uIcc_of_mem_uIccproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

Set.uIcc_injective_leftproof · cited by 0