English
A dependent version of iSup_induction: if the property C depends on an element x and its membership hx in iSup S, and closure under multiplication holds, then C holds for the supremum element.
Русский
Зависимая версия iSup_induction: если свойство C зависит от элемента x и от того, что x принадлежит iSup S, и выполняется замкнутость по умножению, тогда C выполняется для элемента верхнего предела.
LaTeX
$$$(x_1 \\in \\iSup i, S i) \\Rightarrow (\\forall i, \\forall x_2 \\in S i, C x_2) \\,\\rightarrow\\ (\\forall x,y, C x \\rightarrow C y \\rightarrow C(xy)) \\rightarrow C x_1$$$
Lean4
/-- A dependent version of `Subsemigroup.iSup_induction`. -/
@[to_additive (attr := elab_as_elim) /-- A dependent version of `AddSubsemigroup.iSup_induction`. -/
]
theorem iSup_induction' (S : ι → Subsemigroup M) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
(mem : ∀ (i) (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i ‹_›))
(mul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i) : C x₁ hx₁ :=
by
refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁ (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
· exact ⟨_, mem _ _ hx₂⟩
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
exact ⟨_, mul _ _ _ _ Cx Cy⟩
