exists_finset_of_mem_adjoin — Mathlib

English

If x ∈ adjoin F S, there is a finite subset T ⊆ S such that x ∈ adjoin F T.

Русский

Если x ∈ adjoin F S, существует конечное подмножество T ⊆ S с x ∈ adjoin F T.

LaTeX

$$∃ T : Finset E, (T ⊆ S) ∧ x ∈ adjoin F (T : Set E)$$

Lean4

theorem exists_finset_of_mem_adjoin {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
    ∃ T : Finset E, (T : Set E) ⊆ S ∧ x ∈ adjoin F (T : Set E) :=
  by
  simp_rw [← biSup_adjoin_simple S, ← iSup_subtype''] at hx
  obtain ⟨s, hx'⟩ := exists_finset_of_mem_iSup hx
  classical
  refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
  simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]
  rintro _ h _ rfl
  exact subset_adjoin F _ ⟨_, h, rfl⟩

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