English
For an indexed union over a subset s ⊆ β of π-systems g(b), any t in generatePiSystem(⋃ b ∈ s, g(b)) can be expressed using a finite subset T ⊆ s with t = ⋂ b ∈ T f(b) and f(b) ∈ g(b) for all b ∈ T, with the extra constraint that T ⊆ s.
Русский
Для индексированного объединения по подмножеству s ⊆ β π-систем g(b) любой t из generatePiSystem(⋃ b ∈ s, g(b)) может быть выражено через конечное подмножество T ⊆ s с t = ⋂ b ∈ T f(b) и для всех b ∈ T выполняется f(b) ∈ g(b), причём T ⊆ s.
LaTeX
$$$$ \exists T \subseteq s, \exists f: β \to \mathcal P(\alpha), \ t = \bigcap_{b \in T} f(b) \wedge (\forall b \in T, f(b) \in g(b)) $$$$
Lean4
/-- Every element of the π-system generated by an indexed union of a family of π-systems
is a finite intersection of elements from the π-systems.
For a total union version, see `mem_generatePiSystem_iUnion_elim`. -/
theorem mem_generatePiSystem_iUnion_elim' {α β} {g : β → Set (Set α)} {s : Set β} (h_pi : ∀ b ∈ s, IsPiSystem (g b))
(t : Set α) (h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)) :
∃ (T : Finset β) (f : β → Set α), ↑T ⊆ s ∧ (t = ⋂ b ∈ T, f b) ∧ ∀ b ∈ T, f b ∈ g b := by
classical
have : t ∈ generatePiSystem (⋃ b : Subtype s, (g ∘ Subtype.val) b) :=
by
suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b by rwa [h1]
ext x
simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists]
rfl
rcases @mem_generatePiSystem_iUnion_elim α (Subtype s) (g ∘ Subtype.val) (fun b => h_pi b.val b.property) t this with
⟨T, ⟨f, ⟨rfl, h_t'⟩⟩⟩
refine
⟨T.image (fun x : s => (x : β)), Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
· ext a
constructor <;>
· simp -proj only [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
intro h1 b h_b h_b_in_T
have h2 := h1 b h_b h_b_in_T
revert h2
rw [Subtype.val_injective.extend_apply]
apply id
· intro b h_b
simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right] at h_b
obtain ⟨h_b_w, h_b_h⟩ := h_b
have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
rw [h_b_alt, Subtype.val_injective.extend_apply]
apply h_t'
apply h_b_h
