Mathlib Map

Theorems · Theorem · order theory

Set.Bounded.mono

∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Set.Bounded r t → Set.Bounded r s
Defined in
Mathlib.Order.Bounded
Cited by
18 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.bounded_inter_not · cited by 3Set.bounded_inter_notSet.bounded_le_inter_le · cited by 2Set.bounded_le_inter_leSet.bounded_ge_Ioo · cited by 0Set.bounded_ge_IooSet.bounded_gt_Icc · cited by 0Set.bounded_gt_IccSet.bounded_gt_Ico · cited by 0Set.bounded_gt_IcoSet.bounded_gt_Ioc · cited by 0Set.bounded_gt_IocSet.bounded_gt_Ioo · cited by 0Set.bounded_gt_IooSet.bounded_le_Icc · cited by 0Set.bounded_le_IccSet.bounded_le_Ico · cited by 0Set.bounded_le_IcoSet.bounded_le_Ioc · cited by 0Set.bounded_le_IocSet.bounded_le_Ioo · cited by 0Set.bounded_le_IooSet.bounded_lt_Icc · cited by 0Set.bounded_lt_IccSet.bounded_lt_Ico · cited by 0Set.bounded_lt_IcoSet.bounded_lt_Ioc · cited by 0Set.bounded_lt_IocSet.bounded_lt_Ioo · cited by 0Set.bounded_lt_IooSet · cited by 53352SetSet.Bounded · cited by 57Set.BoundedBounded.monoCITED BYCITES

Cites2

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

  • Setstatement and proof · cited by 53,352
  • Set.Boundedstatement and proof · cited by 57

Cited by18

Results whose statement or proof uses this declaration.