Theorems · Theorem · order theory

Set.FiniteExhaustion.mk.injEq

∀ {α : 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

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext