| Metric | Count |
|---|
DefinitionsSublattice, carrier, comap, copy, inclusion, instBot, instCompleteLattice, instDistribLatticeCoe, instInf, instInfCoe, instInfSet, instInhabited, instLatticeCoe, instPartialOrder, instSetLike, instSupCoe, instTop, instUniqueOfIsEmpty, map, ofIsSublattice, pi, prod, prodEquiv, subtype, topEquiv | 25 |
Theoremsapply_coe_mem_map, apply_mem_map_iff, bot_prod, coe_bot, coe_comap, coe_copy, coe_eq_empty, coe_eq_univ, coe_iInf, coe_inclusion, coe_inf, coe_inf', coe_inj, coe_map, coe_mk, coe_pi, coe_prod, coe_sInf, coe_subtype, coe_sup, coe_top, comap_comap, comap_equiv_eq_map_symm, comap_iInf, comap_id, comap_inf, comap_mono, comap_top, copy_eq, ext, gc_map_comap, inclusion_apply, inclusion_injective, inclusion_rfl, infClosed, infClosed', inf_mem, isSublattice, le_comap_iSup, le_comap_sup, le_pi, le_prod_iff, map_bot, map_equiv_eq_comap_symm, map_iSup, map_id, map_inf, map_inf_le, map_le_iff_le_comap, map_map, map_mono, map_sup, map_symm_eq_iff_eq_map, map_top, mem_carrier, mem_comap, mem_iInf, mem_inf, mem_map, mem_map_equiv, mem_map_of_mem, mem_mk, mem_pi, mem_prod, mem_sInf, mem_top, mk_inf_mk, mk_le_mk, mk_lt_mk, mk_sup_mk, notMem_bot, pi_bot, pi_empty, pi_top, pi_univ_bot, pi_univ_eq_bot, pi_univ_eq_bot_iff, prodEquiv_apply, prodEquiv_symm_apply, prodEquiv_toEquiv, prod_bot, prod_eq_bot, prod_eq_top, prod_left_mono, prod_mono, prod_mono_left, prod_mono_right, prod_right_mono, prod_top, subsingleton_iff, subtype_apply, subtype_comp_inclusion, subtype_injective, supClosed, supClosed', sup_mem, top_prod, top_prod_top | 98 |
| Total | 123 |
| Name | Category | Theorems |
|---|
carrier 📖 | CompOp | 8 mathmath: infClosed', BooleanSubalgebra.bot_mem', mem_carrier, CompleteSublattice.mk'_carrier, BooleanSubalgebra.mem_carrier, supClosed', CompleteSublattice.comap_carrier, CompleteSublattice.map_carrier
|
comap 📖 | CompOp | 18 mathmath: comap_inf, map_equiv_eq_comap_symm, map_le_iff_le_comap, comap_id, gc_map_comap, coe_comap, le_comap_iSup, comap_top, le_pi, comap_mono, comap_equiv_eq_map_symm, top_prod, le_prod_iff, le_comap_sup, mem_comap, comap_iInf, prod_top, comap_comap
|
copy 📖 | CompOp | 2 mathmath: coe_copy, copy_eq
|
inclusion 📖 | CompOp | 5 mathmath: subtype_comp_inclusion, inclusion_apply, inclusion_rfl, coe_inclusion, inclusion_injective
|
instBot 📖 | CompOp | 10 mathmath: pi_univ_eq_bot_iff, coe_bot, map_bot, pi_univ_bot, prod_eq_bot, prod_bot, pi_bot, bot_prod, notMem_bot, coe_eq_empty
|
instCompleteLattice 📖 | CompOp | 4 mathmath: le_comap_iSup, map_iSup, le_comap_sup, map_sup
|
instDistribLatticeCoe 📖 | CompOp | — |
instInf 📖 | CompOp | 5 mathmath: comap_inf, mem_inf, coe_inf', map_inf_le, map_inf
|
instInfCoe 📖 | CompOp | 3 mathmath: coe_inf, mk_inf_mk, setLike_mem_inf
|
instInfSet 📖 | CompOp | 5 mathmath: mem_sInf, coe_sInf, coe_iInf, comap_iInf, mem_iInf
|
instInhabited 📖 | CompOp | — |
instLatticeCoe 📖 | CompOp | 10 mathmath: subtype_comp_inclusion, inclusion_apply, subtype_apply, subtype_injective, mem_subtype, inclusion_rfl, coe_inclusion, coe_subtype, inclusion_injective, CompleteSublattice.subtype_apply
|
instPartialOrder 📖 | CompOp | 16 mathmath: map_le_iff_le_comap, mk_le_mk, mk_lt_mk, gc_map_comap, le_comap_iSup, le_pi, BooleanSubalgebra.mk_le_mk, prod_left_mono, comap_mono, inclusion_rfl, BooleanSubalgebra.mk_lt_mk, prod_right_mono, le_prod_iff, map_mono, map_inf_le, le_comap_sup
|
instSetLike 📖 | CompOp | 106 mathmath: BooleanSubalgebra.mem_toSublattice, coe_prod, RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule, BooleanSubalgebra.coe_mk, Module.End.mem_invtSubmodule, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LinearMap.IsProj.mem_invtSubmodule_iff, isSublattice, LinearMap.IsIdempotentElem.commute_iff, coe_map, LinearEquiv.map_mem_invtSubmodule_conj_iff, coe_bot, coe_pi, Submodule.mem_invtSubmodule_reflection_of_mem, mem_prod, RootPairing.invtRootSubmodule.bot_mem, RootPairing.invtRootSubmodule.eq_top_iff, Representation.invtSubmodule.nontrivial_iff, Module.End.mem_invtSubmodule_iff_mapsTo, subtype_comp_inclusion, apply_mem_map_iff, inclusion_apply, mem_sInf, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule, RootPairing.mem_invtRootSubmodule_iff, mem_inf, subtype_apply, coe_inf, coe_inf', Representation.invtSubmodule.coe_top, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, Module.End.invtSubmodule.isCompl_iff, supClosed, apply_coe_mem_map, mem_mk, coe_comap, mem_map, infClosed, RootPairing.invtRootSubmodule.top_mem, prodEquiv_toEquiv, prodEquiv_apply, subtype_injective, setLike_mem_inf, ext_mem_iff, RootPairing.corootSpan_mem_invtSubmodule_coreflection, RootPairing.invtRootSubmodule.eq_bot_iff, coe_inj, mem_subtype, Module.End.isFinitelySemisimple_iff, VonNeumannAlgebra.IsIdempotentElem.mem_iff, inclusion_rfl, VonNeumannAlgebra.IsStarProjection.mem_iff, BooleanSubalgebra.mem_mk, LinearMap.IsIdempotentElem.range_mem_invtSubmodule, Module.AEval.mem_mapSubmodule_symm_apply, Module.End.mem_invtSubmodule_symm_iff_le_map, mem_carrier, RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule, coe_mk, Module.End.span_orbit_mem_invtSubmodule, Module.End.invtSubmodule.codisjoint_iff, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, Representation.invtSubmodule.top_mem, mem_top, ContinuousLinearMap.IsIdempotentElem.commute_iff, coe_inclusion, Set.Mapsto.mem_invtSubmodule, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule, coe_sInf, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem, RootPairing.coe_bot, Module.End.invtSubmodule.top_mem, RootPairing.isIrreducible_iff_invtRootSubmodule, RootPairing.rootSpan_mem_invtSubmodule_reflection, RootPairing.coe_top, mem_pi, Module.End.isSemisimple_iff', notMem_bot, coe_sup, coe_iInf, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, mem_comap, coe_subtype, LinearEquiv.map_mem_invtSubmodule_iff, Representation.invtSubmodule.coe_bot, Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice, coe_eq_empty, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule, coe_top, setLike_mem_coe, Module.End.invtSubmodule.bot_mem, Module.End.mem_invtSubmodule_iff_map_le, inclusion_injective, Module.AEval.mem_mapSubmodule_apply, setLike_mem_sup, prodEquiv_symm_apply, Representation.mem_invtSubmodule, Submodule.mem_invtSubmodule_reflection_iff, mem_map_equiv, CompleteSublattice.subtype_apply, Module.End.invtSubmodule.disjoint_iff, Module.End.isSemisimple_iff, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, coe_eq_univ, mem_iInf, Representation.invtSubmodule.bot_mem
|
instSupCoe 📖 | CompOp | 3 mathmath: coe_sup, mk_sup_mk, setLike_mem_sup
|
instTop 📖 | CompOp | 14 mathmath: pi_top, top_prod_top, comap_top, Module.End.invtSubmodule.one, top_prod, mem_top, map_top, prod_eq_top, Module.End.invtSubmodule.zero, Module.End.invtSubmodule.id, coe_top, pi_empty, prod_top, coe_eq_univ
|
instUniqueOfIsEmpty 📖 | CompOp | — |
map 📖 | CompOp | 20 mathmath: map_equiv_eq_comap_symm, coe_map, map_le_iff_le_comap, apply_mem_map_iff, gc_map_comap, map_map, apply_coe_mem_map, map_bot, mem_map, comap_equiv_eq_map_symm, map_iSup, mem_map_of_mem, map_top, map_mono, map_inf_le, map_symm_eq_iff_eq_map, map_id, mem_map_equiv, map_sup, map_inf
|
ofIsSublattice 📖 | CompOp | — |
pi 📖 | CompOp | 9 mathmath: pi_top, pi_univ_eq_bot_iff, coe_pi, pi_univ_bot, le_pi, pi_bot, mem_pi, pi_univ_eq_bot, pi_empty
|
prod 📖 | CompOp | 18 mathmath: coe_prod, mem_prod, prod_mono_left, prod_mono, top_prod_top, prodEquiv_toEquiv, prodEquiv_apply, prod_eq_bot, prod_left_mono, prod_bot, prod_right_mono, top_prod, bot_prod, le_prod_iff, prod_eq_top, prodEquiv_symm_apply, prod_mono_right, prod_top
|
prodEquiv 📖 | CompOp | 3 mathmath: prodEquiv_toEquiv, prodEquiv_apply, prodEquiv_symm_apply
|
subtype 📖 | CompOp | 6 mathmath: subtype_comp_inclusion, subtype_apply, subtype_injective, mem_subtype, coe_subtype, CompleteSublattice.subtype_apply
|
topEquiv 📖 | CompOp | — |