| Metric | Count |
|---|
DefinitionsPhaseSpace, Fact, IsValid, bang, carrier, linImpl, mk_dual, mk_subset, neg, oplus, parr, quest, tensor, term!_, term_โ
_, withh, ยซterm_&_ยป, ยซterm_แฎยป, ยซterm_โ_ยป, ยซterm_โ_ยป, ยซterm_โธ_ยป, ยซtermส_ยป, I, biorthogonalClosure, bot, carriersInf, dualFact, idempotentsIn, imp, instBotFact, instCoeFactSet, instHasSubsetFact, instInfSetFact, instMinFact, instOneFact, instPartialOrderFact, instSetLikeFact, instTopFact, instZeroFact, interpProp, isFact, orthogonal, toCommMonoid, ยซterm_โซ ยป, ยซtermโฆ_โง_ยป | 45 |
Theoremsbot_par, coe_neg, coe_tensor_assoc, entails_top, entails_with, eq, le_plus_left, le_plus_right, linImpl_bot, linImpl_iff_implies, linImpl_of_par, linImpl_of_tensor, linImpl_par, linImpl_par', mk_dual_coe, mk_subset_coe, mul_subset_tensor, neg_bot, neg_eq_iff, neg_inj, neg_injective, neg_involutive, neg_le_neg_iff, neg_linImpl_neg, neg_neg, neg_one, neg_par, neg_plus, neg_surjective, neg_tensor, neg_top, neg_with, neg_zero, one_linImpl, one_tensor, par_assoc, par_bot, par_comm, par_distrib_with, par_le_par, par_of_linImpl, par_of_tensor, par_semi_distrib_plus, par_top, plus_assoc, plus_comm, plus_entails, plus_eq_with_dual, plus_tensor_distrib, plus_zero, property, tensor_assoc, tensor_assoc_aux, tensor_comm, tensor_distrib_plus, tensor_le_tensor, tensor_linImpl, tensor_of_linImpl, tensor_of_par, tensor_one, tensor_rotate, tensor_semi_distrib_with, tensor_zero, top_par, top_with, valid_with, with_assoc, with_comm, with_eq_plus_dual, with_par_distrib, with_tensor_semi_distrib, with_top, zero_entails, zero_plus, zero_tensor, biorth_least_fact, closed, coe_min, coe_mk, coe_one, coe_top, coe_zero, dualFact_coe, dualFact_empty, dual_dual_subset_Fact_iff, dual_dual_subset_dual_iff, dual_empty, dual_subset_dual, iInter_biorth_eq_orth_iUnion_orth, iInter_eq_sInf_image, inter_eq_orth_union_orth, inter_isFact_of_isFact, isFact_iff_closed, mem_carrier, mem_dual, mem_one, mem_top, mem_zero, mul_mem_one, of_Fact, one_mem_one, orth_antitone, orth_extensive, orth_iUnion, orth_one_eq_bot, orthogonal_def, sInf_isFact, subset_dual_dual, triple_dual, triple_orth, zero_least_fact | 111 |
| Total | 156 |
| Name | Category | Theorems |
|---|
Fact ๐ | CompData | 55 mathmath: Fact.neg_involutive, Fact.neg_bot, Fact.entails_top, dualFact_empty, Fact.neg_le_neg_iff, inter_eq_orth_union_orth, Fact.bot_par, mem_top, mem_carrier, Fact.linImpl_iff_implies, mem_one, Fact.zero_tensor, Fact.par_semi_distrib_plus, Fact.coe_tensor_assoc, coe_mk, Fact.tensor_zero, Fact.eq, zero_least_fact, Fact.top_par, Fact.neg_surjective, Fact.tensor_one, Fact.neg_injective, dualFact_coe, Fact.plus_zero, of_Fact, coe_min, Fact.top_with, Fact.mk_dual_coe, mem_dual, Fact.neg_top, Fact.mk_subset_coe, closed, Fact.zero_entails, Fact.par_bot, one_mem_one, Fact.neg_one, Fact.one_tensor, Fact.coe_neg, Fact.with_top, coe_one, Fact.tensor_semi_distrib_with, Fact.le_plus_left, Fact.linImpl_bot, coe_top, Fact.le_plus_right, Fact.with_tensor_semi_distrib, Fact.one_linImpl, mem_zero, Fact.mul_subset_tensor, dual_dual_subset_Fact_iff, Fact.par_top, Fact.neg_zero, sInf_isFact, coe_zero, Fact.zero_plus
|
I ๐ | CompOp | โ |
biorthogonalClosure ๐ | CompOp | 1 mathmath: isFact_iff_closed
|
bot ๐ | CompOp | 5 mathmath: mem_one, mem_dual, orth_one_eq_bot, coe_one, mem_zero
|
carriersInf ๐ | CompOp | โ |
dualFact ๐ | CompOp | 2 mathmath: dualFact_empty, dualFact_coe
|
idempotentsIn ๐ | CompOp | โ |
imp ๐ | CompOp | 1 mathmath: Fact.linImpl_iff_implies
|
instBotFact ๐ | CompOp | 5 mathmath: Fact.neg_bot, Fact.bot_par, Fact.par_bot, Fact.neg_one, Fact.linImpl_bot
|
instCoeFactSet ๐ | CompOp | โ |
instHasSubsetFact ๐ | CompOp | โ |
instInfSetFact ๐ | CompOp | โ |
instMinFact ๐ | CompOp | 1 mathmath: coe_min
|
instOneFact ๐ | CompOp | 8 mathmath: Fact.neg_bot, mem_one, Fact.tensor_one, one_mem_one, Fact.neg_one, Fact.one_tensor, coe_one, Fact.one_linImpl
|
instPartialOrderFact ๐ | CompOp | 6 mathmath: Fact.neg_le_neg_iff, Fact.par_semi_distrib_plus, Fact.tensor_semi_distrib_with, Fact.le_plus_left, Fact.le_plus_right, Fact.with_tensor_semi_distrib
|
instSetLikeFact ๐ | CompOp | 24 mathmath: inter_eq_orth_union_orth, mem_top, mem_carrier, Fact.linImpl_iff_implies, mem_one, Fact.coe_tensor_assoc, coe_mk, Fact.eq, dualFact_coe, of_Fact, coe_min, Fact.mk_dual_coe, mem_dual, Fact.mk_subset_coe, closed, one_mem_one, Fact.coe_neg, coe_one, coe_top, mem_zero, Fact.mul_subset_tensor, dual_dual_subset_Fact_iff, sInf_isFact, coe_zero
|
instTopFact ๐ | CompOp | 11 mathmath: Fact.entails_top, dualFact_empty, mem_top, Fact.top_par, Fact.top_with, Fact.neg_top, Fact.zero_entails, Fact.with_top, coe_top, Fact.par_top, Fact.neg_zero
|
instZeroFact ๐ | CompOp | 10 mathmath: Fact.zero_tensor, Fact.tensor_zero, zero_least_fact, Fact.plus_zero, Fact.neg_top, Fact.zero_entails, mem_zero, Fact.neg_zero, coe_zero, Fact.zero_plus
|
interpProp ๐ | CompOp | โ |
isFact ๐ | MathDef | 4 mathmath: Fact.property, isFact_iff_closed, closed, sInf_isFact
|
orthogonal ๐ | CompOp | 22 mathmath: triple_dual, inter_eq_orth_union_orth, orth_iUnion, orth_antitone, dual_empty, Fact.coe_tensor_assoc, biorth_least_fact, dual_subset_dual, Fact.eq, Fact.tensor_assoc_aux, subset_dual_dual, orth_extensive, iInter_biorth_eq_orth_iUnion_orth, mem_dual, triple_orth, orth_one_eq_bot, Fact.coe_neg, coe_one, orthogonal_def, dual_dual_subset_dual_iff, dual_dual_subset_Fact_iff, coe_zero
|
toCommMonoid ๐ | CompOp | 9 mathmath: mem_one, Fact.coe_tensor_assoc, Fact.tensor_assoc_aux, mul_mem_one, mem_dual, one_mem_one, orth_one_eq_bot, mem_zero, Fact.mul_subset_tensor
|
ยซterm_โซ ยป ๐ | CompOp | โ |
ยซtermโฆ_โง_ยป ๐ | CompOp | โ |
| Name | Category | Theorems |
|---|
IsValid ๐ | MathDef | 1 mathmath: valid_with
|
bang ๐ | CompOp | โ |
carrier ๐ | CompOp | 3 mathmath: Cslib.CLL.PhaseSpace.mem_carrier, property, Cslib.CLL.PhaseSpace.zero_least_fact
|
linImpl ๐ | CompOp | 15 mathmath: par_of_linImpl, entails_top, linImpl_of_par, tensor_of_linImpl, linImpl_iff_implies, plus_entails, tensor_linImpl, linImpl_of_tensor, linImpl_par', zero_entails, neg_linImpl_neg, entails_with, linImpl_bot, one_linImpl, linImpl_par
|
mk_dual ๐ | CompOp | 1 mathmath: mk_dual_coe
|
mk_subset ๐ | CompOp | 1 mathmath: mk_subset_coe
|
neg ๐ | CompOp | 26 mathmath: neg_neg, neg_involutive, neg_tensor, par_of_tensor, par_of_linImpl, neg_inj, neg_bot, neg_le_neg_iff, linImpl_of_par, tensor_of_linImpl, neg_with, neg_plus, neg_surjective, neg_injective, linImpl_of_tensor, neg_par, plus_eq_with_dual, neg_top, tensor_of_par, neg_one, coe_neg, neg_linImpl_neg, linImpl_bot, with_eq_plus_dual, neg_eq_iff, neg_zero
|
oplus ๐ | CompOp | 14 mathmath: neg_with, par_semi_distrib_plus, tensor_distrib_plus, neg_plus, plus_entails, plus_assoc, plus_comm, plus_zero, plus_eq_with_dual, le_plus_left, plus_tensor_distrib, le_plus_right, with_eq_plus_dual, zero_plus
|
parr ๐ | CompOp | 18 mathmath: neg_tensor, par_of_tensor, par_of_linImpl, linImpl_of_par, bot_par, par_semi_distrib_plus, top_par, linImpl_par', neg_par, par_le_par, par_bot, tensor_of_par, par_comm, with_par_distrib, par_distrib_with, par_assoc, linImpl_par, par_top
|
quest ๐ | CompOp | โ |
tensor ๐ | CompOp | 21 mathmath: neg_tensor, par_of_tensor, tensor_comm, tensor_of_linImpl, zero_tensor, tensor_le_tensor, tensor_distrib_plus, coe_tensor_assoc, tensor_rotate, tensor_zero, tensor_one, tensor_linImpl, linImpl_of_tensor, neg_par, tensor_of_par, one_tensor, tensor_semi_distrib_with, tensor_assoc, plus_tensor_distrib, with_tensor_semi_distrib, mul_subset_tensor
|
term!_ ๐ | CompOp | โ |
term_โ
_ ๐ | CompOp | โ |
withh ๐ | CompOp | 15 mathmath: with_assoc, valid_with, neg_with, neg_plus, plus_entails, top_with, plus_eq_with_dual, with_comm, with_top, tensor_semi_distrib_with, with_par_distrib, entails_with, par_distrib_with, with_tensor_semi_distrib, with_eq_plus_dual
|
ยซterm_&_ยป ๐ | CompOp | โ |
ยซterm_แฎยป ๐ | CompOp | โ |
ยซterm_โ_ยป ๐ | CompOp | โ |
ยซterm_โ_ยป ๐ | CompOp | โ |
ยซterm_โธ_ยป ๐ | CompOp | โ |
ยซtermส_ยป ๐ | CompOp | โ |