AddSubsemigroup.iSup_induction
theorem AddSubsemigroup.iSup_induction :
∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M) {C : M → Prop} {x₁ : M},
x₁ ∈ ⨆ i, S i → (∀ (i : ι), ∀ x₂ ∈ S i, C x₂) → (∀ (x y : M), C x → C y → C (x + y)) → C x₁
This theorem describes an induction principle for elements of the supremum of a collection of additive subsemigroups denoted `⨆ i, S i` in a type `M`. Given a property `C` that holds for all elements `x₂` from all `S i`, and a condition that `C` is preserved under addition (that is, if `C` holds for two elements `x` and `y`, it also holds for their sum `x + y`), the theorem states that if an element `x₁` belongs to the supremum of `S`, then `C` holds for `x₁`.
More concisely: If `S i` is a collection of additive subsemigroups in a type `M`, `x₁` is in the supremum of `S`, and the property `C` holds for all elements `x₂` in `S i` and is preserved under addition, then `C` holds for `x₁`.
|
Subsemigroup.iSup_induction'
theorem Subsemigroup.iSup_induction' :
∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup M) {C : (x : M) → x ∈ ⨆ i, S i → Prop},
(∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
(∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯) →
∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
This theorem, called `Subsemigroup.iSup_induction'`, is a dependent version of `Subsemigroup.iSup_induction`. It states that for any sort `ι` and type `M` with multiplication (`Mul M`), given a function `S` that maps `ι` to subsemigroups of `M`, and a property `C` that holds for elements of the superset of the subsemigroups (denoted `⨆ i, S i`), if `C` holds for every element of each subsemigroup, and if `C` is closed under multiplication in the superset (i.e., `C` holds for the product of any two elements that satisfy `C`), then `C` holds for every element in the superset of the subsemigroups.
More concisely: If `S : ι → Subsemigroup M`, `C : ∀ i, S i → M → Prop`, `∀ i, ∀ x ∈ S i, C x`, and `C` is closed under multiplication in `⨆ i, S i`, then `C` holds for every element in `⨆ i, S i`.
|
Subsemigroup.iSup_induction
theorem Subsemigroup.iSup_induction :
∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M},
x₁ ∈ ⨆ i, S i → (∀ (i : ι), ∀ x₂ ∈ S i, C x₂) → (∀ (x y : M), C x → C y → C (x * y)) → C x₁
This theorem, known as the Subsemigroup induction principle, states that for any indexing type `ι`, any type `M` equipped with a multiplication operation, and any function `S` mapping `ι` into subsemigroups of `M`, if a property `C` is true for all elements of every `S i` and is preserved under multiplication (i.e., if `C` is true for `x` and `y`, then `C` is also true for the product `x*y`), then `C` is also true for any element `x₁` of the supremum of all subsemigroups `S i`.
More concisely: If `S i` is a family of subsemigroups of a type `M` with multiplication, and `C` is a property preserved by multiplication that holds for all elements in each `S i`, then `C` holds for the supremum of all `S i`.
|
AddSubsemigroup.iSup_induction'
theorem AddSubsemigroup.iSup_induction' :
∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → x ∈ ⨆ i, S i → Prop},
(∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
(∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) →
∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
This theorem is a dependent version of `AddSubsemigroup.iSup_induction`. It states that for any indexed set of `AddSubsemigroup` instances of a type `M`, and a property `C` that depends on an element `x` of `M` and a proof that `x` belongs to the supremum of the `AddSubsemigroup` instances, if `C` holds for every element of each individual `AddSubsemigroup`, and if `C` is closed under addition for pairs of elements in the supremum of the `AddSubsemigroups`, then `C` holds for every element in the supremum of the `AddSubsemigroups`.
More concisely: If `M` is an indexed set of `AddSubsemigroups` and `C` is a property that depends on an element `x` of the supremum of `M`, such that `C` holds for every element in each `AddSubsemigroup` and is closed under addition of elements in the supremum, then `C` holds for every element in the supremum of `M`.
|