Basic

📁 Source: Mathlib/Data/Setoid/Basic.lean

Statistics

Metric	Count
Definitions `comap`, `comapQuotientEquiv`, `completeLattice`, `correspondence`, `gi`, `instInfSet`, `instLE_mathlib`, `instMin_mathlib`, `instPartialOrder`, `ker`, `kerLift`, `liftEquiv`, `map`, `mapOfSurjective`, `map_of_le`, `map_sInf`, `piQuotientEquiv`, `prod`, `prodQuotientEquiv`, `quotientKerEquivOfRightInverse`, `quotientKerEquivOfSurjective`, `quotientKerEquivRange`, `quotientKerEquivRangeKerLift`, `quotientQuotientEquivQuotient`, `sigmaQuotientEquivOfLe`	25
Theorems `subsingleton_iff`, `subsingleton_iff`, `bot_def`, `comap_eq`, `comap_rel`, `comm'`, `eq_iff_rel_eq`, `eq_top_iff`, `eqvGen_eq`, `eqvGen_idem`, `eqvGen_le`, `eqvGen_mono`, `eqvGen_of_setoid`, `ext_iff`, `inf_def`, `inf_iff_and`, `injective_iff_ker_bot`, `kerLift_injective`, `kerLift_mk`, `ker_apply_mk_out`, `ker_def`, `ker_eq_lift_of_injective`, `ker_iff_mem_preimage`, `ker_lift_injective`, `ker_mk_eq`, `le_def`, `lift_injective_iff_ker_eq_of_le`, `lift_unique`, `mapOfSurjective_eq_map`, `mk_eq_bot`, `mk_eq_top`, `piQuotientEquiv_apply`, `piQuotientEquiv_symm_apply`, `piSetoid_apply`, `prodQuotientEquiv_apply`, `prodQuotientEquiv_symm_apply`, `prod_apply`, `quotientKerEquivOfRightInverse_apply`, `quotientKerEquivOfRightInverse_symm_apply`, `quotient_mk_sInf_eq`, `range_kerLift_eq_range`, `refl'`, `sInf_def`, `sInf_equiv`, `sInf_iff`, `sSup_def`, `sSup_eq_eqvGen`, `sup_def`, `sup_eq_eqvGen`, `symm'`, `top_def`, `trans'`	52
Total	77

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_iff` 📖	mathematical	—	`Relation.EqvGen` `Top.top` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`Function.Surjective.forall` `mk_surjective` `eq`

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_iff` 📖	mathematical	—	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Setoid.completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Function.Surjective.forall` `mk'_surjective`

Setoid

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	8 math math: `AddAction.orbitRel_le_fst`, `MulAction.orbitRel_le_snd`, `comap_rel`, `MulAction.orbitRel_le_fst`, `AddAction.orbitRel_le_snd`, `SubAddAction.orbitRel_of_subAdd`, `SubMulAction.orbitRel_of_subMul`, `comap_eq`
`comapQuotientEquiv` 📖	CompOp	—
`completeLattice` 📖	CompOp	24 math math: `QuotientAddGroup.leftRel_eq_top`, `AddCon.toSetoid_top`, `AddCon.toSetoid_bot`, `injective_iff_ker_bot`, `top_def`, `sSup_def`, `mk_eq_top`, `sup_eq_eqvGen`, `QuotientAddGroup.rightRel_eq_top`, `Quotient.subsingleton_iff`, `bot_def`, `Con.toSetoid_eq_bot`, `SeparationQuotient.inseparableSetoid_eq_top_iff`, `Con.toSetoid_bot`, `eq_top_iff`, `sup_def`, `QuotientGroup.rightRel_eq_top`, `sSup_eq_eqvGen`, `mk_eq_bot`, `AddCon.toSetoid_eq_bot`, `Con.toSetoid_top`, `Con.toSetoid_eq_top`, `QuotientGroup.leftRel_eq_top`, `AddCon.toSetoid_eq_top`
`correspondence` 📖	CompOp	—
`gi` 📖	CompOp	—
`instInfSet` 📖	CompOp	9 math math: `Con.sInf_toSetoid`, `quotient_mk_sInf_eq`, `RingCon.sInf_toSetoid`, `sInf_equiv`, `sInf_iff`, `continuous_map_sInf`, `eqvGen_eq`, `AddCon.sInf_toSetoid`, `sInf_def`
`instLE_mathlib` 📖	CompOp	9 math math: `AddAction.orbitRel_le_fst`, `eqvGen_le`, `MulAction.orbitRel_le_snd`, `AddAction.orbitRel_addSubgroup_le`, `MulAction.orbitRel_le_fst`, `AddAction.orbitRel_le_snd`, `le_def`, `eqvGen_mono`, `MulAction.orbitRel_subgroup_le`
`instMin_mathlib` 📖	CompOp	2 math math: `inf_iff_and`, `inf_def`
`instPartialOrder` 📖	CompOp	—
`ker` 📖	CompOp	22 math math: `ker_apply_mk_out`, `finite_classes_ker`, `Topology.IsQuotientMap.lift_apply`, `classes_ker_subset_fiber_set`, `Topology.IsQuotientMap.homeomorph_apply`, `ker_iff_mem_preimage`, `Topology.IsQuotientMap.homeomorph_symm_apply`, `injective_iff_ker_bot`, `kerLift_mk`, `quotientKerEquivOfRightInverse_apply`, `kerLift_injective`, `ker_def`, `HomogeneousLocalization.zero_eq`, `ker_mk_eq`, `HomogeneousLocalization.one_eq`, `range_kerLift_eq_range`, `Function.RightInverse.homeomorph_symm_apply`, `card_classes_ker_le`, `quotientKerEquivOfRightInverse_symm_apply`, `ker_lift_injective`, `Function.RightInverse.homeomorph_apply`, `comap_eq`
`kerLift` 📖	CompOp	7 math math: `Topology.IsQuotientMap.homeomorph_apply`, `kerLift_mk`, `quotientKerEquivOfRightInverse_apply`, `kerLift_injective`, `range_kerLift_eq_range`, `ker_lift_injective`, `Function.RightInverse.homeomorph_apply`
`liftEquiv` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `mapOfSurjective_eq_map`
`mapOfSurjective` 📖	CompOp	1 math math: `mapOfSurjective_eq_map`
`map_of_le` 📖	CompOp	1 math math: `continuous_map_of_le`
`map_sInf` 📖	CompOp	1 math math: `continuous_map_sInf`
`piQuotientEquiv` 📖	CompOp	2 math math: `piQuotientEquiv_symm_apply`, `piQuotientEquiv_apply`
`prod` 📖	CompOp	7 math math: `QuotientGroup.rightRel_prod`, `QuotientGroup.leftRel_prod`, `QuotientAddGroup.leftRel_prod`, `prod_apply`, `prodQuotientEquiv_symm_apply`, `prodQuotientEquiv_apply`, `QuotientAddGroup.rightRel_prod`
`prodQuotientEquiv` 📖	CompOp	2 math math: `prodQuotientEquiv_symm_apply`, `prodQuotientEquiv_apply`
`quotientKerEquivOfRightInverse` 📖	CompOp	2 math math: `quotientKerEquivOfRightInverse_apply`, `quotientKerEquivOfRightInverse_symm_apply`
`quotientKerEquivOfSurjective` 📖	CompOp	—
`quotientKerEquivRange` 📖	CompOp	—
`quotientKerEquivRangeKerLift` 📖	CompOp	—
`quotientQuotientEquivQuotient` 📖	CompOp	—
`sigmaQuotientEquivOfLe` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_def` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`comap_eq` 📖	mathematical	—	`comap` `ker` `Quotient.mk''`	—	`ext` `Quotient.eq`
`comap_rel` 📖	mathematical	—	`comap`	—	—
`comm'` 📖	—	—	—	—	`symm'`
`eq_iff_rel_eq` 📖	—	—	—	—	`ext`
`eq_top_iff` 📖	mathematical	—	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`eq_top_iff` `le_def` `top_def`
`eqvGen_eq` 📖	mathematical	—	`Relation.EqvGen.setoid` `InfSet.sInf` `instInfSet` `setOf`	—	`le_antisymm` `refl'` `symm'` `trans'` `sInf_le`
`eqvGen_idem` 📖	mathematical	—	`Relation.EqvGen.setoid`	—	`eqvGen_of_setoid`
`eqvGen_le` 📖	mathematical	—	`instLE_mathlib` `Relation.EqvGen.setoid`	—	`eqvGen_eq` `sInf_le`
`eqvGen_mono` 📖	mathematical	—	`instLE_mathlib` `Relation.EqvGen.setoid`	—	`eqvGen_le`
`eqvGen_of_setoid` 📖	mathematical	—	`Relation.EqvGen.setoid`	—	`le_antisymm` `eqvGen_eq` `sInf_le`
`ext_iff` 📖	—	—	—	—	`ext`
`inf_def` 📖	mathematical	—	`instMin_mathlib` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	—
`inf_iff_and` 📖	mathematical	—	`instMin_mathlib`	—	—
`injective_iff_ker_bot` 📖	mathematical	—	`ker` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`eq_bot_iff`
`kerLift_injective` 📖	mathematical	—	`ker` `kerLift`	—	`Quotient.inductionOn₂'` `Quotient.sound'`
`kerLift_mk` 📖	mathematical	—	`kerLift` `ker`	—	—
`ker_apply_mk_out` 📖	mathematical	—	`Quotient.out` `ker`	—	`Quotient.mk_out`
`ker_def` 📖	mathematical	—	`ker`	—	—
`ker_eq_lift_of_injective` 📖	—	`instLE_mathlib` `ker`	—	—	`le_antisymm`
`ker_iff_mem_preimage` 📖	mathematical	—	`ker` `Set` `Set.instMembership` `Set.preimage` `Set.instSingletonSet`	—	—
`ker_lift_injective` 📖	mathematical	—	`ker` `kerLift`	—	`kerLift_injective`
`ker_mk_eq` 📖	mathematical	—	`ker` `Quotient.mk''`	—	`ext` `Quotient.eq`
`le_def` 📖	mathematical	—	`instLE_mathlib`	—	—
`lift_injective_iff_ker_eq_of_le` 📖	—	`instLE_mathlib` `ker`	—	—	`ker_eq_lift_of_injective` `kerLift_injective`
`lift_unique` 📖	—	`instLE_mathlib` `ker` `Quotient.mk''`	—	—	—
`mapOfSurjective_eq_map` 📖	mathematical	`instLE_mathlib` `ker`	`map` `mapOfSurjective`	—	`eqvGen_of_setoid`
`mk_eq_bot` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`mk_eq_top` 📖	mathematical	—	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`piQuotientEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `piSetoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `piQuotientEquiv` `Quotient.mk''` `Quotient.out`	—	—
`piQuotientEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `piSetoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `piQuotientEquiv` `Quotient.liftOn'` `Quotient.mk''`	—	—
`piSetoid_apply` 📖	mathematical	—	`piSetoid`	—	—
`prodQuotientEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `prod` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodQuotientEquiv` `Quotient.map₂`	—	—
`prodQuotientEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `prod` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodQuotientEquiv` `Quotient.liftOn'` `Quotient.mk''`	—	—
`prod_apply` 📖	mathematical	—	`prod`	—	—
`quotientKerEquivOfRightInverse_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ker` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientKerEquivOfRightInverse` `kerLift`	—	—
`quotientKerEquivOfRightInverse_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ker` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `quotientKerEquivOfRightInverse` `Quotient.mk''`	—	—
`quotient_mk_sInf_eq` 📖	mathematical	—	`InfSet.sInf` `instInfSet`	—	—
`range_kerLift_eq_range` 📖	mathematical	—	`Set.range` `ker` `kerLift`	—	`Set.range_quotient_lift`
`refl'` 📖	—	—	—	—	—
`sInf_def` 📖	mathematical	—	`InfSet.sInf` `instInfSet` `Pi.infSet` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Prop.instCompleteLattice` `Set.image`	—	`sInf_image` `iInf_apply` `iInf_Prop_eq`
`sInf_equiv` 📖	mathematical	—	`InfSet.sInf` `instInfSet`	—	—
`sInf_iff` 📖	mathematical	—	`InfSet.sInf` `instInfSet`	—	—
`sSup_def` 📖	mathematical	—	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `completeLattice` `Relation.EqvGen.setoid` `Pi.supSet` `Prop.instCompleteLattice` `Set.image`	—	`sSup_eq_eqvGen` `sSup_image` `iSup_apply` `iSup_Prop_eq`
`sSup_eq_eqvGen` 📖	mathematical	—	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `completeLattice` `Relation.EqvGen.setoid` `Set` `Set.instMembership`	—	`eqvGen_eq` `Set.ext`
`sup_def` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `Relation.EqvGen.setoid` `Pi.instMaxForall_mathlib` `Prop.instCompleteLattice`	—	`sup_eq_eqvGen`
`sup_eq_eqvGen` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `Relation.EqvGen.setoid`	—	`eqvGen_eq`
`symm'` 📖	—	—	—	—	—
`top_def` 📖	mathematical	—	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`trans'` 📖	—	—	—	—	—

---

← Back to Index