lean_problem_sheets / 2019.questions.sheet1

theorem question_one (P Q : Prop) :

P ∧ Q → Q ∧ P

Note: this declaration is incomplete and uses sorry.

theorem question_2a_true (P Q : Prop) :

(P → Q) → Q → P

Note: this declaration is incomplete and uses sorry.

theorem question_2a_false :

¬∀ (P Q : Prop), (P → Q) → Q → P

Note: this declaration is incomplete and uses sorry.

theorem question_2b_true (P Q : Prop) :

(P ↔ Q) → (Q ↔ P)

Note: this declaration is incomplete and uses sorry.

theorem question_2b_false :

¬∀ (P Q : Prop), (P ↔ Q) → (Q ↔ P)

Note: this declaration is incomplete and uses sorry.

theorem question_3_true (P Q R : Prop) (h1 : Q → P) (h2 : ¬Q → ¬R) :

R → P

Note: this declaration is incomplete and uses sorry.

theorem question_3_false :

¬∀ (P Q R : Prop), (Q → P) → (¬Q → ¬R) → R → P

Note: this declaration is incomplete and uses sorry.

theorem question_4 (P Q R : Prop) (h1 : P → Q ∧ R) (h2 : Q → R ∧ ¬P) (h3 : R → P ∧ ¬Q) :

P ∨ Q

Note: this declaration is incomplete and uses sorry.

theorem question_5 (P : ℤ → Prop) (h8 : ∀ (n : ℤ), P n → P (n + 8)) (h3 : ∀ (n : ℤ), P n → P (n - 3)) :

(∀ (n : ℤ), P n) ∨ ∀ (n : ℤ), ¬P n

Note: this declaration is incomplete and uses sorry.