Mathlib Map

Theorems · Theorem · order theory

Set.Ico_subset_Icc_self

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico b a ⊆ Set.Icc b a
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
41 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.Ioo_subset_Icc_self · cited by 54Set.Ioo_subset_Icc_selfConvex.norm_image_sub_le_of_norm_hasFDerivWithin_le · cited by 9Convex.norm_image_sub_le_…Set.mem_Icc_of_Ico · cited by 4Set.mem_Icc_of_Icoclosure_Ico · cited by 4closure_IcoIcc_mem_nhdsGE_of_mem · cited by 4Icc_mem_nhdsGE_of_memnorm_image_sub_le_of_norm_deriv_le_segment' · cited by 4norm_image_sub_le_of_norm…image_le_of_liminf_slope_right_lt_deriv_boundary' · cited by 4image_le_of_liminf_slope_…isLUB_Ico · cited by 3isLUB_IcoStrictAntiOn.mapsTo_Ico · cited by 2StrictAntiOn.mapsTo_IcoAddConstMapClass.rel_map_of_Icc · cited by 2AddConstMapClass.rel_map_…ODE_solution_unique_of_mem_Ioo · cited by 2ODE_solution_unique_of_me…nhdsGE_basis_Icc · cited by 2nhdsGE_basis_IccFinset.Ico_subset_Icc_self · cited by 2Finset.Ico_subset_Icc_selfOrderEmbedding.image_Ico · cited by 2OrderEmbedding.image_IcoIoi_mem_nhdsSet_Ico · cited by 2Ioi_mem_nhdsSet_IcoSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Icc · cited by 1702Set.Iccle_of_lt · cited by 1175le_of_ltSet.Ico · cited by 799Set.IcoSet.Ico_subset_Icc_selfCITED BYCITES

Cites5

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

  • Setstatement · cited by 53,352
  • Preorderstatement and proof · cited by 7,952
  • Set.Iccstatement · cited by 1,702
  • le_of_ltproof · cited by 1,175
  • Set.Icostatement · cited by 799

Cited by41

Results whose statement or proof uses this declaration.