iUnion_decode₂_cases — Mathlib

English

If C is a property of sets with C(∅) and if ∀ b, C(f(b)) holds, then for every n, C(⋃ b ∈ decode₂ β n, f(b)).

Русский

Пусть C — свойство множеств, удовлетворяющее C(∅) и C(f(b)) для каждого b. Тогда для любого n выполняется C(⋃ b ∈ decode₂ β n, f(b)).

LaTeX

$$$ C\\big(\\bigcup_{b \\in decode_2(\\beta,n)} f(b)\\big) \\\\text{ provided } C(\\emptyset)\\text{ and } \\forall b,\\, C(f(b)). $$$

Lean4

@[elab_as_elim]
theorem iUnion_decode₂_cases {f : β → Set α} {C : Set α → Prop} (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
    C (⋃ b ∈ decode₂ β n, f b) :=
  match decode₂ β n with
  | none => by
    simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]
    apply H0
  | some b => by
    convert H1 b
    simp

Похожие утверждения