Analysis I, Appendix A.1: Mathematical Statements

An introduction to mathematical statements. Showcases some basic tactics and Lean syntax.

def Exercise_A_1_3 : Decidable (∀ (X Y : Prop), (X → Y) → (¬X → ¬Y) → (X ↔ Y))

Exercise A.1.3.

Equations

• Exercise_A_1_3 = sorry

def Exercise_A_1_4 : Decidable (∀ (X Y : Prop), (X → Y) → (¬Y → ¬X) → (X ↔ Y))

Exercise A.1.4.

Equations

• Exercise_A_1_4 = sorry

def Exercise_A_1_5 : Decidable (∀ (X Y Z : Prop), (X ↔ Y) → (Y ↔ Z) → [X, Y, Z].TFAE)

Exercise A.1.5.

Equations

• Exercise_A_1_5 = sorry

def Exercise_A_1_6 : Decidable (∀ (X Y Z : Prop), (X → Y) → (Y → Z) → (Z → X) → [X, Y, Z].TFAE)

Exercise A.1.6.

Equations

• Exercise_A_1_6 = sorry