【Lean4】intro

intro

「任意の〜について」や「〜ならば」を証明するときに、変数や仮定を導入する

全称命題の例

Plaintext

example : ∀ n : ℕ, n = n := by
  intro n
  rfl
  
/-
最初の目標は、
⊢ ∀ n : ℕ, n = n
だったが、intro nの後は、
n : ℕ
⊢ n = n
になる
-/

example : ∀ n : ℕ, n = n := by
  intro n
  rfl
  
/-
最初の目標は、
⊢ ∀ n : ℕ, n = n
だったが、intro nの後は、
n : ℕ
⊢ n = n
になる
-/

含意の例

Plaintext

example (P Q : Prop) : P → Q → P := by
  intro hP
  intro hQ
  exact hP

example (P Q : Prop) : P → Q → P := by
  intro hP
  intro hQ
  exact hP