induction_of_closure_eq_top_left — Mathlib

English

A more elaborate left-induction principle for closure: given a motive, if it is true for 1 and closed under left-multiplication by elements of s, it holds for all of closure(s).

Русский

Уточнённый принцип левой индукции по замыканию: если свойство верно для 1 и сохраняется при левом умножении на элементы s, то выполняется для всего closure(s).

LaTeX

$$$\\text{closure_induction_left} \\ (s,motive,one,mul_left,x,h) : \\text{motive } x\\;h $$$

Lean4

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

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