induction_on_adjoin_finset — Mathlib

English

Let S be a finite set and P a property of intermediate fields. If P holds for ⊥ and if P(K) implies P(K⟮x⟯.restrictScalars F) whenever x ∈ S, then P(adjoin F S) holds.

Русский

Пусть S — конечное множество и P — свойство подполь, такое что P⊥ истинно, и если для K ∈ IntermediateField и x ∈ S из P(K) следует P(K⟮x⟯.restrictScalars F), тогда P(adjoin F S) истинно.

LaTeX

$$$P(\operatorname{adjoin}_F S) \text{ holds given base and step condition on elements of } S$$$

Lean4

theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥)
    (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) : P (adjoin F S) := by
  classical
  refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
  · simp [base]
  · rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
    exact ih (adjoin F _) _ ha h

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