@[protected]
theorem
quot.lift_beta
{α : Sort u}
{r : α → α → Prop}
{β : Sort v}
(f : α → β)
(c : ∀ (a b : α), r a b → f a = f b)
(a : α) :
quot.lift f c (quot.mk r a) = f a
@[protected]
theorem
quot.ind_beta
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Prop}
(p : ∀ (a : α), β (quot.mk r a))
(a : α) :
_ = _
@[protected]
def
quot.lift_on
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
(q : quot r)
(f : α → β)
(c : ∀ (a b : α), r a b → f a = f b) :
β
@[protected]
theorem
quot.induction_on
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Prop}
(q : quot r)
(h : ∀ (a : α), β (quot.mk r a)) :
β q
@[protected]
def
quot.indep
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Sort v}
(f : Π (a : α), β (quot.mk r a))
(a : α) :
psigma β
Equations
- quot.indep f a = ⟨quot.mk r a, f a⟩
@[protected]
theorem
quot.indep_coherent
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Sort v}
(f : Π (a : α), β (quot.mk r a))
(h : ∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b)
(a b : α) :
r a b → quot.indep f a = quot.indep f b
@[protected]
theorem
quot.lift_indep_pr1
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Sort v}
(f : Π (a : α), β (quot.mk r a))
(h : ∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b)
(q : quot r) :
(quot.lift (quot.indep f) _ q).fst = q
@[protected]
def
quot.rec_on_subsingleton
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Sort v}
[h : ∀ (a : α), subsingleton (β (quot.mk r a))]
(q : quot r)
(f : Π (a : α), β (quot.mk r a)) :
β q
Equations
- q.rec_on_subsingleton f = quot.rec f _ q
Instances for quotient
- t2_space_of_properly_discontinuous_smul_of_t2_space
- t2_space_of_properly_discontinuous_vadd_of_t2_space
- quotient.inhabited
- quotient.subsingleton
- quotient.fintype
- dfinsupp.fun_like
- dfinsupp.has_coe_to_fun
- dfinsupp.has_zero
- dfinsupp.inhabited
- dfinsupp.has_add
- dfinsupp.add_zero_class
- dfinsupp.has_nat_scalar
- dfinsupp.add_monoid
- dfinsupp.add_comm_monoid
- dfinsupp.has_neg
- dfinsupp.has_sub
- dfinsupp.has_int_scalar
- dfinsupp.add_group
- dfinsupp.add_comm_group
- dfinsupp.has_scalar
- dfinsupp.smul_comm_class
- dfinsupp.is_scalar_tower
- dfinsupp.is_central_scalar
- dfinsupp.distrib_mul_action
- dfinsupp.module
- dfinsupp.unique
- dfinsupp.has_add₂
- dfinsupp.add_zero_class₂
- dfinsupp.add_monoid₂
- dfinsupp.distrib_mul_action₂
- quotient_group.fintype_quotient_right_rel
- quotient_add_group.fintype_quotient_right_rel
- dfinsupp.add_comm_monoid_of_linear_map
- dfinsupp.module_of_linear_map
- module.free.dfinsupp
- quotient.topological_space
- quotient.compact_space
- uniform_space.separation_setoid.uniform_space
- uniform_space.separated_separation
- has_dist_metric_quot
- metric_space_quot
- quotient.measurable_space
- uniform_space.complete_space_separation
- sym2.has_mem
- sym2.subsingleton
- sym2.unique
- sym2.is_empty
- sym2.nontrivial
- dfinsupp.has_le
- dfinsupp.preorder
- dfinsupp.partial_order
- dfinsupp.semilattice_inf
- dfinsupp.semilattice_sup
- dfinsupp.lattice
- dfinsupp.ordered_add_comm_monoid
- dfinsupp.ordered_cancel_add_comm_monoid
- dfinsupp.has_le.le.contravariant_class
- dfinsupp.order_bot
- dfinsupp.tsub
- dfinsupp.has_ordered_sub
- dfinsupp.canonically_ordered_add_monoid
- dfinsupp.locally_finite_order
- fin_enum.quotient.enum
- quotient.finite
- first_order.language.quotient_structure
- uniform_space.comm_ring
- uniform_space.topological_ring
- game.add_comm_group_with_one
- game.inhabited
- game.partial_order
- game.lf.is_trichotomous
- game.covariant_class_add_le
- game.covariant_class_swap_add_le
- game.covariant_class_add_lt
- game.covariant_class_swap_add_lt
- game.ordered_add_comm_group
- slim_check.total_function.dfinsupp.sampleable_ext
@[protected]
Equations
- quotient.lift f = quot.lift f
@[protected]
def
quotient.lift_on
{α : Sort u}
{β : Sort v}
[s : setoid α]
(q : quotient s)
(f : α → β)
(c : ∀ (a b : α), a ≈ b → f a = f b) :
β
Equations
- q.lift_on f c = quot.lift_on q f c
@[protected]
def
quotient.rec_on_subsingleton
{α : Sort u}
[s : setoid α]
{β : quotient s → Sort v}
[h : ∀ (a : α), subsingleton (β ⟦a⟧)]
(q : quotient s)
(f : Π (a : α), β ⟦a⟧) :
β q
Equations
@[protected]
def
quotient.lift₂
{α : Sort u_a}
{β : Sort u_b}
{φ : Sort u_c}
[s₁ : setoid α]
[s₂ : setoid β]
(f : α → β → φ)
(c : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
(q₁ : quotient s₁)
(q₂ : quotient s₂) :
φ
Equations
- quotient.lift₂ f c q₁ q₂ = quotient.lift (λ (a₁ : α), quotient.lift (f a₁) _ q₂) _ q₁
@[protected]
def
quotient.lift_on₂
{α : Sort u_a}
{β : Sort u_b}
{φ : Sort u_c}
[s₁ : setoid α]
[s₂ : setoid β]
(q₁ : quotient s₁)
(q₂ : quotient s₂)
(f : α → β → φ)
(c : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) :
φ
Equations
- q₁.lift_on₂ q₂ f c = quotient.lift₂ f c q₁ q₂
@[protected]
@[protected]
def
quotient.rec_on_subsingleton₂
{α : Sort u_a}
{β : Sort u_b}
[s₁ : setoid α]
[s₂ : setoid β]
{φ : quotient s₁ → quotient s₂ → Sort u_c}
[h : ∀ (a : α) (b : β), subsingleton (φ ⟦a⟧ ⟦b⟧)]
(q₁ : quotient s₁)
(q₂ : quotient s₂)
(f : Π (a : α) (b : β), φ ⟦a⟧ ⟦b⟧) :
φ q₁ q₂
Equations
- q₁.rec_on_subsingleton₂ q₂ f = q₁.rec_on_subsingleton (λ (a : α), q₂.rec_on_subsingleton (λ (b : β), f a b))
- rel : ∀ {α : Type u} {r : α → α → Prop} (x y : α), r x y → eqv_gen r x y
- refl : ∀ {α : Type u} {r : α → α → Prop} (x : α), eqv_gen r x x
- symm : ∀ {α : Type u} {r : α → α → Prop} (x y : α), eqv_gen r x y → eqv_gen r y x
- trans : ∀ {α : Type u} {r : α → α → Prop} (x y z : α), eqv_gen r x y → eqv_gen r y z → eqv_gen r x z
theorem
quot.exact
{α : Type u}
(r : α → α → Prop)
{a b : α}
(H : quot.mk r a = quot.mk r b) :
eqv_gen r a b
theorem
quot.eqv_gen_sound
{α : Type u}
{r : α → α → Prop}
{a b : α}
(H : eqv_gen r a b) :
quot.mk r a = quot.mk r b
@[protected, instance]
def
quotient.decidable_eq
{α : Sort u}
{s : setoid α}
[d : Π (a b : α), decidable (a ≈ b)] :
decidable_eq (quotient s)
Equations
- quotient.decidable_eq = λ (q₁ q₂ : quotient s), q₁.rec_on_subsingleton₂ q₂ (λ (a₁ a₂ : α), quotient.decidable_eq._match_1 a₁ a₂ (d a₁ a₂))
- quotient.decidable_eq._match_1 a₁ a₂ (decidable.is_true h₁) = decidable.is_true _
- quotient.decidable_eq._match_1 a₁ a₂ (decidable.is_false h₂) = decidable.is_false _