English
An induction principle for proving a property for any element of the supremum of a family of Subalgebras: if a property is closed under 0, 1, addition, multiplication, and algebra maps, and holds for elements coming from each S_i, then it holds for every element of ⨆ i, S_i.
Русский
Принцип индукции по верхнему пределу: если свойство сохраняется под 0, 1, сложение, умножение и отображение алгебр, и верно для элементов каждого S_i, то верно и для любого элемента ⨆ i, S_i.
LaTeX
$$iSup_induction(S, motive, mem) : motive x mem$$
Lean4
@[elab_as_elim]
theorem iSup_induction {ι : Sort*} (S : ι → Subalgebra R A) {motive : A → Prop} {x : A} (mem : x ∈ ⨆ i, S i)
(basic : ∀ i, ∀ a ∈ S i, motive a) (zero : motive 0) (one : motive 1)
(add : ∀ a b, motive a → motive b → motive (a + b)) (mul : ∀ a b, motive a → motive b → motive (a * b))
(algebraMap : ∀ r, motive (algebraMap R A r)) : motive x :=
by
let T : Subalgebra R A :=
{ carrier := {x | motive x}
mul_mem' {a b} := mul a b
one_mem' := one
add_mem' {a b} := add a b
zero_mem' := zero
algebraMap_mem' := algebraMap }
suffices iSup S ≤ T from this mem
rwa [iSup_le_iff]
