Theorems · Definition · order theory

Set.FiniteExhaustion.mk.noConfusion

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

Defined in

Mathlib.Data.Set.FiniteExhaustion

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms