【Lean4】rcases

rcases

存在命題、連言、部分型などを分解するときに使う

Plaintext

example (P : ℕ → Prop)
    (h : ∃ n, P n) :
    ∃ n, P n := by
  rcases h with ⟨n, hn⟩
  exact ⟨n, hn⟩
  

/-
rcases h with ⟨n, hn⟩により
証人n
その性質の証明hn : P n
を取り出す
-/

example (P : ℕ → Prop)
    (h : ∃ n, P n) :
    ∃ n, P n := by
  rcases h with ⟨n, hn⟩
  exact ⟨n, hn⟩
  

/-
rcases h with ⟨n, hn⟩により
証人n
その性質の証明hn : P n
を取り出す
-/

Lean4の関連記事

【Lean4】namespace
【Lean4】section
【Lean4】variable
【Lean4】abbrev
【Lean4】constructor
【Lean4】#check
【Lean4】def
【Lean4】exact
【Lean4】rfl
【Lean4】intro
【Lean4】apply
【Lean4】unfold
【Lean4】rw
【Lean4】simp
【Lean4】simpa
【Lean4】constructor
【Lean4】left,right
【Lean4】cases
【Lean4】rcases
【Lean4】refine
【Lean4】use
【Lean4】have
【Lean4】show
【Lean4】change
【Lean4】subst
【Lean4】by_cases
【Lean4】induction
【Lean4】ext
【Lean4】funext
【Lean4】congrArg
【Lean4】norm_num
【Lean4】ring
【Lean4】linarith
【Lean4】aesop
【Lean4】structure
【Lean4】where
【Lean4】@[simp]
【Lean4】 #eval
【Lean4】let
【Lean4】if（条件分岐）
【Lean4】match（パターンマッチ）
【Lean4】リスト
【Lean4】Option
【Lean4】inductive