mathlib documentation

lean_problem_sheets / 2019.questions.sheet4

inductive Q1a.X :

Type

one : Q1a.X
two : Q1a.X

def Q1a.X.R :

Q1a.X → Q1a.X → Prop

Equations

theorem Q1a.X.Q1a_refl :

reflexive Q1a.X.R

Note: this declaration is incomplete and uses sorry.

theorem Q1a.X.Q1a_symm :

symmetric Q1a.X.R

Note: this declaration is incomplete and uses sorry.

theorem Q1a.X.Q1a_trans :

transitive Q1a.X.R

Note: this declaration is incomplete and uses sorry.

theorem Q1a.X.Q1a_equiv :

equivalence Q1a.X.R

Note: this declaration is incomplete and uses sorry.

def Q1b.R (a b : ℝ) :

Prop

Equations

Q1b.R a b = (a = -b)

theorem Q1b.Q1b_refl :

reflexive Q1b.R

Note: this declaration is incomplete and uses sorry.

theorem Q1b.Q1b_symm :

symmetric Q1b.R

Note: this declaration is incomplete and uses sorry.

theorem Q1b.Q1b_trans :

transitive Q1b.R

Note: this declaration is incomplete and uses sorry.

theorem Q1b.Q1b_equiv :

equivalence Q1b.R

Note: this declaration is incomplete and uses sorry.

def Q1c.R (a b : ℝ) :

Prop

Equations

Q1c.R a b = false

theorem Q1c.Q1c_refl :

reflexive Q1c.R

Note: this declaration is incomplete and uses sorry.

theorem Q1c.Q1c_symm :

symmetric Q1c.R

Note: this declaration is incomplete and uses sorry.

theorem Q1c.Q1c_trans :

transitive Q1c.R

Note: this declaration is incomplete and uses sorry.

theorem Q1c.Q1c_equiv :

equivalence Q1c.R

Note: this declaration is incomplete and uses sorry.

def Q1d.R (a b : empty) :

Prop

Equations

Q1d.R a b = empty.cases_on (λ (a : empty), Prop) a

theorem Q1d.Q1d_refl :

reflexive Q1d.R

Note: this declaration is incomplete and uses sorry.

theorem Q1d.Q1d_symm :

symmetric Q1d.R

Note: this declaration is incomplete and uses sorry.

theorem Q1d.Q1d_trans :

transitive Q1d.R

Note: this declaration is incomplete and uses sorry.

theorem Q1d.Q1d_equiv :

equivalence Q1d.R

Note: this declaration is incomplete and uses sorry.

def Q2a :

partial_order (set ℤ)

Equations

Q2a = {le := λ (A B : set ℤ), A ⊆ B, lt := preorder.lt._default (λ (A B : set ℤ), A ⊆ B), le_refl := Q2a._proof_1, le_trans := Q2a._proof_2, lt_iff_le_not_le := Q2a._proof_3, le_antisymm := Q2a._proof_4}

Note: this declaration is incomplete and uses sorry.

theorem Q2b :

is_total (set ℤ) (λ (A B : set ℤ), A ⊆ B)

Note: this declaration is incomplete and uses sorry.

theorem Q3a :

symmetric (λ (a b : ℝ), a < b)

Note: this declaration is incomplete and uses sorry.

theorem Q3b :

symmetric (λ (a b : ↥∅), a < b)

Note: this declaration is incomplete and uses sorry.

theorem Q4 (X : Type) (R : X → X → Prop) (hs : symmetric R) (ht : transitive R) :

Note: this declaration is incomplete and uses sorry.

def pals {X Y Z : Type} (f : X → Y) (g : X → Z) :

Prop

Equations

pals f g = ∃ (h : Y → Z), function.bijective h ∧ g = h ∘ f