sometimes_spec — Mathlib

English

If P is a property on α, f : p → α, a : p, and P (f a) holds, then P (Sometimes f) also holds.

Русский

Если существует свойство P на α такое, что P(f a) истинно, тогда P(Sometimes f) тоже истинно.

LaTeX

$$$ \forall {p} {\alpha} [\operatorname{Nonempty} \alpha] (P : \alpha \to \operatorname{Prop}) (f : p \to \alpha) (a : p) (h : P (f a)),\; P (\operatorname{Sometimes} f)$$$

Lean4

theorem sometimes_spec {p : Prop} {α} [Nonempty α] (P : α → Prop) (f : p → α) (a : p) (h : P (f a)) : P (sometimes f) :=
  by rwa [sometimes_eq]

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