Theorems · Definition · order theory

PrincipalSeg.casesOn

{α : Type u_4} →
  {β : Type u_5} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        {motive : PrincipalSeg r s → Sort u} →
          (t : PrincipalSeg r s) →
            ((toRelEmbedding : r ↪r s) →
                (top : β) →
                  (mem_range_iff_rel' : ∀ (b : β), b ∈ Set.range ⇑toRelEmbedding ↔ s b top) →
                    motive { toRelEmbedding := toRelEmbedding, top := top, mem_range_iff_rel' := mem_range_iff_rel' }) →
              motive t

Defined in

Mathlib.Order.InitialSeg

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms