wellFoundedOn_sup — Mathlib

English

If s is a finite index set and f(i) are sets, then (s.sup f) is WF iff each f(i) is WF.

Русский

Если индексы конечного множества s и f(i) — множества, то (s.sup f) является WF тогда и только тогда, когда каждое f(i) является WF.

LaTeX

$$$(s.sup f).WellFoundedOn\\, r \\iff \\forall i\\in s, (f(i)).WellFoundedOn\\, r$$$

Lean4

theorem wellFoundedOn_sup [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} :
    (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r :=
  Finset.cons_induction_on s (by simp) fun a s ha hs => by simp [-sup_set_eq_biUnion, hs]

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