partiallyWellOrderedOn_sup — Mathlib

English

For finite s, (s.sup f) is PartiallyWellOrderedOn r iff each f(i) is PartiallyWellOrderedOn r.

Русский

Для конечного множества s, (s.sup f) частично хорошо упорядовано по r тогда и только тогда, когда каждое f(i) частично хорошо упорядовано по r.

LaTeX

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

Lean4

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

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