mathlib documentation

lean_problem_sheets / 2019.questions.sheet2

source
theorem question1 (Ω : Type) (X Y : set Ω) :
X ∩ Y = Y ∩ X

Note: this declaration is incomplete and uses sorry.

source
def U  :
set ℕ
Equations
  • U = {1, 2, 3, 4, 5}
source
theorem question2a_true  :
1 ∈ U

Note: this declaration is incomplete and uses sorry.

source
theorem question2c_true  :
{1} ⊆ U

Note: this declaration is incomplete and uses sorry.

source
theorem question2d_true  :
{1, 2} ⊆ U

Note: this declaration is incomplete and uses sorry.

source
theorem question2e_true  :
{1, 2, 1} ⊆ U

Note: this declaration is incomplete and uses sorry.

source
theorem question2h_true  :
U ⊇ U

Note: this declaration is incomplete and uses sorry.

source
def A  :
set ℝ
Equations
source
def B  :
set ℝ
Equations
source
def C  :
set ℝ
Equations
source
theorem question3a_true  :
1 / 2 ∈ A ∩ B

Note: this declaration is incomplete and uses sorry.

source
theorem question3b_true  :
1 / 2 ∈ A ∪ B

Note: this declaration is incomplete and uses sorry.

source
theorem question3c_true  :
A ⊆ C

Note: this declaration is incomplete and uses sorry.

source
theorem question3d_true  :
B ⊆ C

Note: this declaration is incomplete and uses sorry.

source
theorem question3e_true  :
C ⊆ A ∪ B

Note: this declaration is incomplete and uses sorry.

source
theorem question3f_true  :
A ∩ B ∪ C = (A ∪ B) ∩ C

Note: this declaration is incomplete and uses sorry.

source
theorem question4a (X : Type) (P Q : X → Prop) :
(¬∀ (x : X), P x ∧ ¬Q x) ↔ true

Note: this declaration is incomplete and uses sorry.

source
theorem question4b (X : Type) (P Q : X → Prop) :
(¬∃ (x : X), ¬P x ∧ Q x) ↔ true

Note: this declaration is incomplete and uses sorry.

source
theorem question4c (X Y : Type) (R : X → Y → Prop) :
(¬∀ (x : X), ∃ (y : Y), R x y) ↔ true

Note: this declaration is incomplete and uses sorry.

source
theorem question5a_true (x : ℝ) :
∃ (y : ℝ), x + y = 2

Note: this declaration is incomplete and uses sorry.

source
theorem question5b_true  :
∃ (y : ℝ), ∀ (x : ℝ), x + y = 2

Note: this declaration is incomplete and uses sorry.

source
theorem question6a_true  :
∃ (x : ℕ) (H : x ∈ ∅), 2 + 2 = 5

Note: this declaration is incomplete and uses sorry.

source
theorem question6b_true (x : ℕ) (H : x ∈ ∅) :
2 + 2 = 5

Note: this declaration is incomplete and uses sorry.