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]