ax9_ext_fonctionnelle

Énoncé

∀ {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : ∀ (x : α), f x = g x), f = g

Deux fonctions qui prennent partout la même valeur sont égales.

Axiomes consommés

C’est un axiome : il est admis, pas démontré. Tout ce qui s’appuie dessus en hérite, et c’est précisément ce que cette bibliothèque rend visible.

• ax9_ext_fonctionnelle

Code

/-- **Axiome 9.** Deux fonctions qui coïncident partout sont égales.
C'est ce qui donne l'égalité des parties de ℝ vues comme prédicats `ℝ → Prop`, c'est-à-dire
le type même sur lequel portent `estMajorant`, `estBorneSup` et `ax7_completude`. -/
axiom ax9_ext_fonctionnelle {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g