algebraicIndependent_sUnion_of_directed

English

There exists a maximal algebraically independent subset u of t containing s, with u ⊆ t, under Zorn’s lemma.

Русский

Существует максимальная алгебраически независимая подмножество u, содержащее s и включающееся в t, существование доказано с помощью леммы Цорна.

LaTeX

$$$\exists u,\ s \subseteq u \land \Maximal(\lambda x, AlgebraicIndependent R x \land x \subseteq t)\ u$$$

Lean4

theorem algebraicIndependent_sUnion_of_directed {s : Set (Set A)} (hsn : s.Nonempty) (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, AlgebraicIndependent R ((↑) : a → A)) : AlgebraicIndependent R ((↑) : ⋃₀ s → A) :=
  by
  letI : Nonempty s := Nonempty.to_subtype hsn
  rw [sUnion_eq_iUnion]
  exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)

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