Mathlib Map

Theorems · Theorem · order theory

iSup_Prop_eq

∀ {ι : Sort u_4} {p : ι → Prop}, ⨆ i, p i = ∃ i, p i
Defined in
Mathlib.Order.CompleteLattice.Basic
Cited by
12 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.ObjectProperty.prop_iSup_iff · cited by 3ObjectProperty.prop_iSup_…hasCardinalLT_iUnion · cited by 2hasCardinalLT_iUnionhasCardinalLT_subtype_iSup · cited by 2hasCardinalLT_subtype_iSupMeasurableSpace.exists_eq_iUnion_countablyGeneratedAtom · cited by 1MeasurableSpace.exists_eq…binary_relation_sSup_iff · cited by 0binary_relation_sSup_iffSetoid.sSup_def · cited by 0Setoid.sSup_defCategoryTheory.MorphismProperty.sSup_iff · cited by 0MorphismProperty.sSup_iffCon.sSup_eq_conGen · cited by 0Con.sSup_eq_conGenRingCon.sSup_eq_ringConGen · cited by 0RingCon.sSup_eq_ringConGenunary_relation_sSup_iff · cited by 0unary_relation_sSup_iffAddCon.sSup_eq_addConGen · cited by 0AddCon.sSup_eq_addConGenScott.isOpen_sUnion · cited by 0Scott.isOpen_sUnioniSup · cited by 2415iSuple_antisymm · cited by 2068le_antisymmiSup_Prop_eqCITED BYCITES

Cites2

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

  • iSupstatement and proof · cited by 2,415
  • le_antisymmproof · cited by 2,068

Cited by12

Results whose statement or proof uses this declaration.