Theorems · Definition · order theory

Set.FiniteExhaustion.noConfusion

{P : Sort u} →
  {α : Type u_1} →
    {s : Set α} →
      {t : s.FiniteExhaustion} →
        {α' : Type u_1} →
          {s' : Set α'} →
            {t' : s'.FiniteExhaustion} → α = α' → s ≍ s' → t ≍ t' → Set.FiniteExhaustion.noConfusionType P t t'

Defined in

Mathlib.Data.Set.FiniteExhaustion

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms