Theorems · Definition

Function.sometimes

{α : Sort u_1} → {β : Sort u_2} → [Nonempty β] → (α → β) → β

sometimes f evaluates to some value of f, if it exists. This function is especially interesting in the case where α is a proposition, in which case f is necessarily a constant function, so that sometimes f = f a for all a.

Defined in

Mathlib.Logic.Function.Basic

Cited by

86 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Nonempty