mathlib documentation

lean_problem_sheets / 2020.relations.equiv_partition2

structure partition (X : Type u_1) :

Type u_1

ℱ : set (set X)
disjoint : ∀ (A B : set X), A ∈ self.ℱ → B ∈ self.ℱ → A ≠ B → A ∩ B = ∅
cover : ∀ (x : X), ∃ (A : set X) (H : A ∈ self.ℱ), x ∈ A
nonempty : ∀ (A : set X), A ∈ self.ℱ → A ≠ ∅

def always_true (X : Type u_1) :

X → X → Prop

Equations

always_true X = λ (a b : X), true

theorem always_true_refl (X : Type u_1) :

reflexive (always_true X)

theorem always_true_symm (X : Type u_1) :

symmetric (always_true X)

theorem always_true_trans (X : Type u_1) :

transitive (always_true X)

theorem always_true_equiv (X : Type u_1) :

equivalence (always_true X)

def always_true_setoid (X : Type u_1) :

Equations

always_true_setoid X = {r := always_true X, iseqv := _}

def F {X : Type u_1} (S : setoid X) :

Equations

F S = sorry

Note: this declaration is incomplete and uses sorry.

def G {X : Type u_1} (P : partition X) :

Equations

G P = sorry

Note: this declaration is incomplete and uses sorry.

theorem FG_eq_id {X : Type u_1} (P : partition X) :

F (G P) = P

Note: this declaration is incomplete and uses sorry.

theorem GF_eq_id {X : Type u_1} (S : setoid X) :

G (F S) = S

Note: this declaration is incomplete and uses sorry.

def partitions_biject_with_equivalence_relations {X : Type u_1} :

setoid X ≃ partition X

Equations

partitions_biject_with_equivalence_relations = sorry

Note: this declaration is incomplete and uses sorry.