induction_on — Mathlib

English

As in trStmts₁_supports, but with a variant handling a union with K; if H1 holds and H2 and H3 as in the statement, then trStmts₁ q ∪ K is supported.

Русский

Как и в trStmts₁_supports, но с вариантом, работающим с объединением с K; если выполнены условия H1, H2 и H3, то trStmts₁ q ∪ K поддерживается.

LaTeX

$$$\\text{trStmts₁}(q) \\cup K \\subseteq S \\text{ и } (K \\subseteq S \\rightarrow \\mathrm{Supports}(K,S)) \\Rightarrow \\mathrm{Supports}(\\mathrm{trStmts₁}(q) \\cup K, S).$$$

Lean4

@[elab_as_elim]
protected theorem induction_on {Γ} [Inhabited Γ] {p : ListBlank Γ → Prop} (q : ListBlank Γ)
    (h : ∀ a, p (ListBlank.mk a)) : p q :=
  Quotient.inductionOn' q h

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