DeZero.and_left

Énoncé

∀ {a : Prop} {b : Prop} (h : a ∧ b), a

D’une conjonction, ne retient que sa moitié gauche.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Projection gauche. -/
theorem and_left {a b : Prop} (h : a ∧ b) : a :=
  And.rec (motive := fun _ => a) (fun ha _ => ha) h