snd

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Exists.snd

English

For any h : Exists p, p h.fst holds; that is, from the existence of a witness to p, p of that witness holds.

Русский

Для любого h : Exists p верно p h.fst; то есть существование свидетеля p для некоторого элемента e удовлетворяет p(e).

LaTeX

$$$\forall h:\Exists p,\ p\bigl(h\.fst\bigr)$$$

Lean4

theorem snd {b : Prop} {p : b → Prop} : ∀ h : Exists p, p h.fst
  | ⟨_, h⟩ => h

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

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

Разделы

Аффилиация

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