Projects.Util.Quotient

source

theorem Quot.lift_mk_of {α : Type u_1} {P : α → α → Prop} {f : α → Prop} {a : α} (h₁ : ∀ (a b : α), P a b → f a = f b) (h₂ : (∀ (a₁ a₂ : α), P a₁ a₂ → f a₁ = f a₂) → f a) :

lift f h₁ (mk P a)

source

theorem Setoid.commFn {α : Type u_1} (s : Setoid α) :

⇑s = fun (x y : α) => s y x

source

theorem liftWith_aux₁ {α : Type u_1} {β : Type u_2} {s : Setoid α} {f : α → β} {x y : α} (h : x ≈ y) :

(fun (x_1 : ∀ (a b : α), s ⟦x⟧.out a → s ⟦x⟧.out b → f a = f b) => f x) ≍ fun (x : ∀ (a b : α), s ⟦y⟧.out a → s ⟦y⟧.out b → f a = f b) => f y

source

def Quotient.liftWith {α : Type u_1} {β : Type u_2} {s : Setoid α} (q : Quotient s) (f : α → β) (h : ∀ (x y : α), s q.out x → s q.out y → f x = f y) :

Equations

q.liftWith f h = Quotient.hrecOn (motive := fun (q : Quotient s) => (∀ (x y : α), s q.out x → s q.out y → f x = f y) → β) q (fun (a : α) (h : ∀ (x y : α), s ⟦a⟧.out x → s ⟦a⟧.out y → f x = f y) => f a) ⋯ h

Instances For

source

theorem Quotient.apply_of {α : Type u_1} [s : Setoid α] {p : α → Prop} {q : Quotient s} {h : ∀ (a b : α), a ≈ b → p a = p b} :

p q.out ↔ Quotient.lift p h q

source

@[simp]

theorem Quotient.mk_out_eq {α : Type u_1} {s : Setoid α} {q : Quotient s} :

Quot.mk (⇑s) q.out = q

source

theorem Quotient.eq_mk_out {α : Type u_1} {s : Setoid α} {q : Quotient s} :

q = Quot.mk (⇑s) q.out

source

theorem Quotient.mk_eq_mk {α : Type u_1} {s : Setoid α} {x y : α} :

⟦x⟧ = ⟦y⟧ ↔ s x y

source

theorem Quot.mk_eq_mk {α : Type u_1} {s : Setoid α} {x y : α} :

mk (⇑s) x = mk (⇑s) y ↔ s x y

source

@[simp]

theorem Quot.mk_out_equiv {α : Type u_1} {s : Setoid α} {x : α} :

s (mk (⇑s) x).out x

source

@[simp]

theorem Quot.equiv_mk_out {α : Type u_1} {s : Setoid α} {x : α} :

s x (mk (⇑s) x).out

source

theorem quot_aux₁ {α : Type u_1} {β : α → Type u_2} {s : Setoid α} {f : (i : α) → β i} (h : ∀ (x y : α), s x y → f x ≍ f y) (x : α) :

β x = β (Quot.mk (⇑s) x).out

source

theorem quot_aux₂ {α : Type u_1} {β : α → Type u_2} {s : Setoid α} {f : (i : α) → β i} (h : ∀ (x y : α), s x y → f x ≍ f y) (a b : α) (p : s a b) :

⋯ ▸ (fun (x : α) => cast ⋯ (f x)) a = (fun (x : α) => cast ⋯ (f x)) b

source

theorem Quot.rec_eq_apply_out {α : Type u_1} {β : α → Type u_2} {s : Setoid α} {q : Quot ⇑s} {f : (i : α) → β i} (h : ∀ (x y : α), s x y → f x ≍ f y) :

Quot.rec (fun (x : α) => cast ⋯ (f x)) ⋯ q = f q.out

source

theorem Quot.ndrec_eq_apply_out {α : Type u_1} {β : Type u_2} {s : Setoid α} {q : Quot ⇑s} {f : α → β} {h : ∀ (a b : α) (p : s a b), ⋯ ▸ f a = f b} :

Quot.rec f h q = f q.out

source

theorem Quotient.rec_eq_apply_out {α : Type u_1} {β : α → Type u_2} {s : Setoid α} {q : Quotient s} {f : (i : α) → β i} (h : ∀ (x y : α), s x y → f x ≍ f y) :

Quotient.rec (fun (x : α) => cast ⋯ (f x)) ⋯ q = f q.out

source

theorem Quotient.ndrec_eq_apply_out {α : Type u_1} {β : Type u_2} {s : Setoid α} {q : Quotient s} {f : α → β} {h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b} :

Quotient.rec f h q = f q.out

source

@[simp]

theorem Quot.mk_out_equiv_iff {α : Type u_1} {s : Setoid α} {x y : α} :

s (mk (⇑s) x).out y ↔ s x y

source

@[simp]

theorem Quot.equiv_mk_out_iff {α : Type u_1} {s : Setoid α} {x y : α} :

s x (mk (⇑s) y).out ↔ s x y

source

def liftWith_aux₂ {α : Type u_1} {β : Type u_2} {s : Setoid α} (q : Quotient s) (f : α → β) (h : ∀ (x y : α), s x q.out → s y q.out → f x = f y) :

Equations

liftWith_aux₂ q f h = Quotient.hrecOn (motive := fun (q : Quotient s) => (∀ (x y : α), s x q.out → s y q.out → f x = f y) → β) q (fun (a : α) (h : ∀ (x y : α), s x ⟦a⟧.out → s y ⟦a⟧.out → f x = f y) => f a) ⋯ h

Instances For

source

@[simp]

theorem liftWith_aux₃ {α : Type u_1} {β : Type u_2} {s : Setoid α} {q : Quotient s} {f : α → β} {h : ∀ (x y : α), s x q.out → s y q.out → f x = f y} :

liftWith_aux₂ q f h = f q.out

source

@[simp]

theorem Quotient.liftWith_eq {α : Type u_1} {β : Type u_2} {s : Setoid α} {q : Quotient s} {f : α → β} {h : ∀ (x y : α), s q.out x → s q.out y → f x = f y} :

q.liftWith f h = f q.out

source

theorem Quotient.lift_eq {α : Type u_1} {β : Type u_2} {s : Setoid α} {q : Quotient s} {f : α → β} {h : ∀ (x y : α), s x y → f x = f y} :

Quotient.lift f h q = f q.out

source

@[simp]

theorem Quotient.out_equiv {α : Type u_1} {s : Setoid α} {x : α} :

⟦x⟧.out ≈ x

source

@[simp]

theorem Quotient.equiv_out {α : Type u_1} {s : Setoid α} {x : α} :

x ≈ ⟦x⟧.out

source

theorem Quotient.apply_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Setoid α} {q : Quotient s} {f : β → γ} {g : α → β} {h₁ : ∀ (a b : α), a ≈ b → g a = g b} (h₂ : ∀ (a b : α), a ≈ b → f (g a) = f (g b)) :

f (Quotient.lift g h₁ q) = Quotient.lift (f ∘ g) h₂ q