Mathlib Map

Theorems · Theorem · order theory

Set.Iio_eq_empty_iff

∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio a = ∅ ↔ IsMin a
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
5 results in Mathlib
Foundations
Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsMin.Iio_eq · cited by 11IsMin.Iio_eqdisjointed_of_isMin · cited by 1disjointed_of_isMinWithBot.bot_covBy_coe · cited by 1WithBot.bot_covBy_coeWithBot.bot_wcovBy_coe · cited by 0WithBot.bot_wcovBy_coeLowerSet.Iio_eq_bot · cited by 0LowerSet.Iio_eq_botSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Iio · cited by 1166Set.IioIsMin · cited by 277IsMinSet.Iio_eq_empty_iffCITED 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
  • Preorderstatement and proof · cited by 7,952
  • Set.Iiostatement · cited by 1,166
  • IsMinstatement · cited by 277

Cited by5

Results whose statement or proof uses this declaration.