sometimes_eq — Mathlib

English

For a Prop p, a type α, and a nonempty α, and f : p → α, we have sometimes f = f a for any a : p.

Русский

Для пропозиции p и типа α существует иногда-значение функции, удовлетворяющее равенству sometimes f = f a для любого a : p.

LaTeX

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

Lean4

theorem sometimes_eq {p : Prop} {α} [Nonempty α] (f : p → α) (a : p) : sometimes f = f a :=
  dif_pos ⟨a⟩

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