induction_of_closure_eq_top_right

English

If closure(s) = ⊤, then for any x, assuming P(1) and the left-multiplicative closure step, P holds for x.

Русский

Если closure(s) = ⊤, то для любого x при условии P(1) и шага слева умножения P выполняется для x.

LaTeX

$$$\\text{If } \\operatorname{closure}(s) = \\top,\\ \\forall x,\\ motive\\ 1\\ \\Rightarrow\\ (\\forall x\\in s)(x\\cdot y)\\ to\\ motive\\; $$$

Lean4

@[to_additive (attr := elab_as_elim)]
theorem induction_of_closure_eq_top_right {s : Set M} {motive : M → Prop} (hs : closure s = ⊤) (x : M) (one : motive 1)
    (mul_right : ∀ x, ∀ y ∈ s, motive x → motive (x * y)) : motive x :=
  by
  have : x ∈ closure s := by simp [hs]
  induction this using closure_induction_right with
  | one => exact one
  | mul_right x _ y hy ih => exact mul_right x y hy ih

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