elim_to_inhabited

Mathlib.Logic.Nonempty

URI: https://scilib.ai/kg/mathlib#Nonempty.elim_to_inhabited

English

From a nonempty α and a function f from Inhabited α to p, one obtains p.

Русский

Из непустого α и функции f : Inhabited α → p следует p.

LaTeX

$$$\forall {\alpha : Type*} [\,h : Nonempty \alpha] {p : Prop} (f : Inhabited \alpha \to p), p$$$

Lean4

theorem elim_to_inhabited {α : Sort*} [h : Nonempty α] {p : Prop} (f : Inhabited α → p) : p :=
  h.elim <| f ∘ Inhabited.mk

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru