Mathlib Map

Theorems · Theorem · order theory

bddAbove_iff_subset_Iic

∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove s ↔ ∃ a, s ⊆ Set.Iic a
Defined in
Mathlib.Order.Bounds.Basic
Cited by
2 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

bddAbove_slope_gt_of_mem_interior · cited by 2bddAbove_slope_gt_of_mem_…ciSup_prod · cited by 2ciSup_prodSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Iic · cited by 1111Set.IicBddAbove · cited by 620BddAbovebddAbove_iff_subset_IicCITED BYCITES

Cites4

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
  • Preorderstatement and proof · cited by 7,952
  • Set.Iicstatement · cited by 1,111
  • BddAbovestatement · cited by 620

Cited by2

Results whose statement or proof uses this declaration.