exists_maximal_algebraicIndependent

English

Same directed-union principle as 173804, stated for a second instance.

Русский

Та же идея направленного объединения, повторенная во втором случае.

LaTeX

$$$\text{AlgebraicIndependent}_R (\bigcup_i s_i) \text{ при DirectedOn и независимости на каждом } s_i$$$

Lean4

theorem exists_maximal_algebraicIndependent (s t : Set A) (hst : s ⊆ t) (hs : AlgebraicIndepOn R id s) :
    ∃ u, s ⊆ u ∧ Maximal (fun (x : Set A) ↦ AlgebraicIndepOn R id x ∧ x ⊆ t) u :=
  by
  refine
    zorn_subset_nonempty {u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
      (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩
  · exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)
  exact fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy

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