0afb9e732c
Former-commit-id: bdede6ed1b6f578f2ef046c338caf02d0b29d453 [formerly 7187de361b53e9c8ec121df379b762f2db736ea2] Former-commit-id: 447d58460fbbfd05ffe08428a1288e392637561d
10 lines
213 B
Lean4
10 lines
213 B
Lean4
import logic
|
|
section
|
|
variables (A : Type) (p q : A → Prop)
|
|
|
|
example : (∀x : A, p x ∧ q x) → ∀y : A, p y :=
|
|
assume H : ∀x : A, p x ∧ q x,
|
|
take y : A,
|
|
show p y, from and.elim_left (H y)
|
|
end
|