Mathlib Map

Theorems · Theorem · order theory

Set.uIcc_subset_uIcc_union_uIcc

∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c

A sort of triangle inequality.

Defined in
Mathlib.Order.Interval.Set.UnorderedInterval
Cited by
4 results in Mathlib
Foundations
Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.mem_ordConnectedComponent_trans · cited by 2Set.mem_ordConnectedCompo…Set.ordConnected_of_uIcc_subset_left · cited by 1Set.ordConnected_of_uIcc_…Finset.uIcc_subset_uIcc_union_uIcc · cited by 0Finset.uIcc_subset_uIcc_u…Set.disjoint_ordT5Nhd · cited by 0Set.disjoint_ordT5NhdSet · cited by 53352SetLinearOrder · cited by 8572LinearOrderSet.uIcc · cited by 393Set.uIccle_total · cited by 294le_totalSet.uIcc_subset_uIcc_union_uI…CITED BYCITES

Cites4

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

  • Setstatement · cited by 53,352
  • LinearOrderstatement and proof · cited by 8,572
  • Set.uIccstatement and proof · cited by 393
  • le_totalproof · cited by 294

Cited by4

Results whose statement or proof uses this declaration.