Theorems · Definition · order theory

Set.FiniteExhaustion.casesOn

{α : Type u_1} →
  {s : Set α} →
    {motive : s.FiniteExhaustion → Sort u} →
      (t : s.FiniteExhaustion) →
        ((toFun : ℕ → Set α) →
            (finite' : ∀ (n : ℕ), Finite ↑(toFun n)) →
              (subset_succ' : ∀ (n : ℕ), toFun n ⊆ toFun (n + 1)) →
                (iUnion_eq' : ⋃ n, toFun n = s) →
                  motive
                    { toFun := toFun, finite' := finite', subset_succ' := subset_succ', iUnion_eq' := iUnion_eq' }) →
          motive t

Defined in

Mathlib.Data.Set.FiniteExhaustion

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms