sUnion — Mathlib

English

IsRelLowerSet.sUnion: union over a set of sets preserves IsRelLowerSet.

Русский

IsRelLowerSet.sUnion: объединение по множеству множеств сохраняет IsRelLowerSet.

LaTeX

$$$\\forall S, \\forall hS, IsRelLowerSet s P \\Rightarrow IsRelLowerSet S.\\!sUnion P$$$

Lean4

protected theorem sUnion {S : Set (Set α)} (hS : ∀ s ∈ S, IsRelLowerSet s P) : IsRelLowerSet (⋃₀ S) P :=
  fun _ ⟨s, ms, mb⟩ ↦ ⟨(hS s ms mb).1, fun _ x y ↦ ⟨s, ms, (hS s ms mb).2 x y⟩⟩

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