| Name | Category | Theorems |
|---|
Antivary 📖 | MathDef | 49 mathmath: Monotone.antivary, monovary_inv_left, antivary_iff_smul_rearrangement, antivary_inv₀, Monovary.dual_left, Antitone.antivary, antivary_inv, Monovary.of_inv_left, monovary_toDual_right, monovary_inv_right₀, Monovary.of_neg_left, antivary_inv_right₀, Monovary.inv_right, antivaryOn_univ, Monovary.neg_right, antivary_neg, Monovary.inv_left, antivary_toDual_right, antivary_iff_exists_monotone_antitone, Monovary.inv_right₀, Monovary.inv_left₀, antivary_inv_left, Monovary.dual_right, antivaryOn_iff_antivary, antivary_neg_left, antivary_iff_mul_rearrangement, antivary_id_iff, antivary_const_right, monovary_toDual_left, Monovary.of_inv_right, Monovary.comp_antitone_left, antivary_toDual_left, antivary_iff_forall_mul_nonpos, Subsingleton.antivary, Monovary.of_inv_right₀, monovary_inv_left₀, antivary_iff_forall_smul_nonpos, antivary_comm, monovary_neg_right, monovary_inv_right, antivary_const_left, Monovary.of_inv_left₀, Monovary.of_neg_right, antivary_neg_right, antivary_inv_left₀, monovary_neg_left, antivary_iff_exists_antitone_monotone, antivary_inv_right, Monovary.neg_left
|
AntivaryOn 📖 | MathDef | 52 mathmath: antivaryOn_comm, MonovaryOn.inv_right, MonovaryOn.of_inv_right, antivaryOn_toDual_left, antivaryOn_inv_left₀, antivaryOn_inv_right, AntitoneOn.antivaryOn, MonovaryOn.dual_left, antivaryOn_const_left, monovaryOn_inv_right, MonovaryOn.of_neg_left, MonovaryOn.of_inv_left, antivaryOn_neg_left, MonovaryOn.inv_left₀, antivaryOn_univ, MonovaryOn.inv_right₀, MonovaryOn.dual_right, antivaryOn_iff_exists_monotoneOn_antitoneOn, monovaryOn_toDual_right, monovaryOn_neg_right, antivaryOn_inv₀, MonovaryOn.of_inv_left₀, MonovaryOn.comp_antitoneOn_right, monovaryOn_neg_left, antivaryOn_inv, MonotoneOn.antivaryOn, antivaryOn_iff_antivary, AntivaryOn.empty, antivaryOn_inv_left, antivaryOn_iff_smul_rearrangement, MonovaryOn.of_inv_right₀, antivaryOn_neg, monovaryOn_inv_left₀, antivaryOn_id_iff, antivaryOn_iff_forall_mul_nonpos, antivaryOn_toDual_right, MonovaryOn.neg_right, antivaryOn_neg_right, antivaryOn_iff_exists_antitoneOn_monotoneOn, antivaryOn_const_right, antivaryOn_iff_forall_smul_nonpos, antivaryOn_iff_mul_rearrangement, MonovaryOn.inv_left, MonovaryOn.of_neg_right, antivaryOn_inv_right₀, MonovaryOn.comp_antitone_on_left, MonovaryOn.neg_left, monovaryOn_toDual_left, monovaryOn_inv_right₀, Antivary.antivaryOn, monovaryOn_inv_left, Subsingleton.antivaryOn
|
Monovary 📖 | MathDef | 50 mathmath: Antivary.inv_right, monovary_inv, monovary_iff_mul_rearrangement, monovary_inv_left, Antivary.neg_right, Antivary.of_neg_right, monovary_toDual_right, monovary_inv_right₀, Antivary.inv_right₀, monovaryOn_iff_monovary, Antivary.neg_left, Antivary.dual_left, Antivary.inv_left₀, antivary_inv_right₀, monovary_iff_forall_smul_nonneg, monovary_neg, antivary_toDual_right, monovary_iff_smul_rearrangement, monovary_comm, monovary_iff_exists_antitone, Antivary.of_inv_left₀, monovary_self, antivary_inv_left, Antivary.of_inv_left, Monotone.monovary, antivary_neg_left, monovary_id_iff, monovary_const_left, monovary_const_right, monovaryOn_univ, monovary_iff_forall_mul_nonneg, monovary_toDual_left, monovary_inv₀, Antivary.of_inv_right, antivary_toDual_left, Antivary.dual_right, Antitone.monovary, monovary_inv_left₀, monovary_neg_right, monovary_inv_right, Subsingleton.monovary, antivary_neg_right, Antivary.inv_left, antivary_inv_left₀, monovary_neg_left, antivary_inv_right, Antivary.comp_antitone_left, Antivary.of_inv_right₀, monovary_iff_exists_monotone, Antivary.of_neg_left
|
MonovaryOn 📖 | MathDef | 53 mathmath: AntivaryOn.comp_antitoneOn_right, AntivaryOn.of_inv_right₀, monovaryOn_inv₀, Monovary.monovaryOn, AntivaryOn.neg_left, AntivaryOn.inv_left₀, antivaryOn_toDual_left, monovaryOn_inv, antivaryOn_inv_left₀, AntitoneOn.monovaryOn, AntivaryOn.dual_right, monovaryOn_comm, antivaryOn_inv_right, monovaryOn_neg, monovaryOn_const_right, monovaryOn_iff_forall_smul_nonneg, monovaryOn_iff_monovary, monovaryOn_inv_right, monovaryOn_self, antivaryOn_neg_left, MonovaryOn.empty, AntivaryOn.of_neg_right, monovaryOn_iff_exists_monotoneOn, monovaryOn_toDual_right, monovaryOn_neg_right, AntivaryOn.comp_antitone_on_left, monovaryOn_iff_smul_rearrangement, monovaryOn_neg_left, antivaryOn_inv_left, monovaryOn_univ, AntivaryOn.of_inv_left₀, monovaryOn_inv_left₀, Subsingleton.monovaryOn, monovaryOn_id_iff, AntivaryOn.dual_left, MonotoneOn.monovaryOn, antivaryOn_toDual_right, AntivaryOn.inv_right₀, AntivaryOn.neg_right, AntivaryOn.of_neg_left, antivaryOn_neg_right, monovaryOn_const_left, monovaryOn_iff_exists_antitoneOn, monovaryOn_iff_mul_rearrangement, AntivaryOn.of_inv_left, AntivaryOn.inv_right, AntivaryOn.inv_left, antivaryOn_inv_right₀, AntivaryOn.of_inv_right, monovaryOn_toDual_left, monovaryOn_inv_right₀, monovaryOn_inv_left, monovaryOn_iff_forall_mul_nonneg
|