Theorems · Definition · order theory

Order.Ideal.casesOn

{P : Type u_2} →
  [inst : LE P] →
    {motive : Order.Ideal P → Sort u} →
      (t : Order.Ideal P) →
        ((toLowerSet : LowerSet P) →
            (nonempty' : toLowerSet.carrier.Nonempty) →
              (directed' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier) →
                motive { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' }) →
          motive t

Defined in: Mathlib.Order.Ideal
Cited by: 1 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms
Assumes: LE

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Set.Nonemptystatement and proof · cited by 2,627
DirectedOnstatement and proof · cited by 271
LowerSetstatement and proof · cited by 230
Order.Idealstatement and proof · cited by 102
LowerSet.carrierstatement and proof · cited by 11

Cited by3

Results whose statement or proof uses this declaration.

Order.Ideal.toLowerSet_injectiveproof · cited by 1
Order.Ideal.noConfusionproof · cited by 0
Order.Ideal.noConfusionTypeproof · cited by 0