intro

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#BEx.intro

English

If a ∈ α with h₁ : p a and h₂ : P a h₁, then ∃ x : α, ∃ h : p x, P x h.

Русский

Если a ∈ α и h₁ : p(a) и h₂ : P(a, h₁), тогда существует x ∈ α и h : p x такие, что P x h.

LaTeX

$$$(a : \alpha) (h1 : p(a)) (h2 : P(a,h1)) \to \exists x:\, \exists h: p x, P x h$$

Lean4

theorem intro (a : α) (h₁ : p a) (h₂ : P a h₁) : ∃ (x : _) (h : p x), P x h :=
  ⟨a, h₁, h₂⟩

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

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

Разделы

Аффилиация

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