cases_on — Mathlib

English

To prove a property for all elements of WithOne α, it suffices to check it for 1 and for all a ∈ α.

Русский

Чтобы доказать свойство для всех элементов WithOne α, достаточно проверить его для 1 и для всех a ∈ α.

LaTeX

$$$\forall x : WithOne α, P(1) \to (\forall a : α, P(a)) \to P(x)$$$

Lean4

@[to_additive (attr := elab_as_elim)]
protected theorem cases_on {P : WithOne α → Prop} : ∀ x : WithOne α, P 1 → (∀ a : α, P a) → P x :=
  Option.casesOn

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