Theorems · Theorem · order theory

Set.FiniteExhaustion.mk.inj

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

Defined in

Mathlib.Data.Set.FiniteExhaustion

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms