Mathlib Map

Theorems · Definition · order theory

Set.Bounded

{α : Type u} → (α → α → Prop) → Set α → Prop

A bounded or final set. Not to be confused with Bornology.IsBounded.

Defined in
Mathlib.Order.RelClasses
Cited by
57 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.Bounded.mono · cited by 18Bounded.monoSet.not_bounded_iff · cited by 7Set.not_bounded_iffSet.bounded_self · cited by 4Set.bounded_selfSet.bounded_gt_Ioi · cited by 3Set.bounded_gt_IoiSet.bounded_inter_not · cited by 3Set.bounded_inter_notSet.bounded_le_inter_lt · cited by 3Set.bounded_le_inter_ltSet.bounded_lt_Iio · cited by 3Set.bounded_lt_IioSet.bounded_lt_inter_not_lt · cited by 3Set.bounded_lt_inter_not_…Set.bounded_ge_Ioi · cited by 2Set.bounded_ge_IoiSet.bounded_gt_Ici · cited by 2Set.bounded_gt_IciSet.bounded_le_Iic · cited by 2Set.bounded_le_IicSet.bounded_le_Iio · cited by 2Set.bounded_le_IioSet.bounded_le_iff_bounded_lt · cited by 2Set.bounded_le_iff_bounde…Set.bounded_le_inter_le · cited by 2Set.bounded_le_inter_leSet.bounded_le_inter_not_le · cited by 2Set.bounded_le_inter_not_…Set · cited by 53352SetSet.BoundedCITED BYCITES

Cites1

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

Cited by58

Results whose statement or proof uses this declaration.