Basic

📁 Source: Mathlib/Order/Heyting/Basic.lean

Statistics

Metric	Count
Definitions BiheytingAlgebra, toCoheytingAlgebra, toHNot, toHeytingAlgebra, toSDiff, CoheytingAlgebra, ofHNot, ofSDiff, toBoundedOrder, toDistribLattice, toGeneralizedCoheytingAlgebra, toHNot, toOrderTop, biheytingAlgebra, coheytingAlgebra, generalizedCoheytingAlgebra, generalizedHeytingAlgebra, heytingAlgebra, GeneralizedCoheytingAlgebra, toDistribLattice, toLattice, toOrderBot, toSDiff, GeneralizedHeytingAlgebra, toDistribLattice, toHImp, toLattice, toOrderTop, HeytingAlgebra, ofCompl, ofHImp, toBoundedOrder, toCompl, toGeneralizedHeytingAlgebra, toOrderBot, toBiheytingAlgebra, instBiheytingAlgebra, instCoheytingAlgebra, instGeneralizedCoheytingAlgebra, instGeneralizedHeytingAlgebra, instHeytingAlgebra, instBiheytingAlgebra, instBiheytingAlgebra, instCoheytingAlgebra, instGeneralizedCoheytingAlgebra, instGeneralizedHeytingAlgebra, instHImpForall, instHNotForall, instHeytingAlgebra, instBiheytingAlgebra, instCoheytingAlgebra, instCompl, instGeneralizedCoheytingAlgebra, instGeneralizedHeytingAlgebra, instHImp, instHNot, instHeytingAlgebra, instSDiff, instHeytingAlgebra	59
Theorems sdiff_le_iff, top_sdiff, himp_eq_left, himp_eq_right, himp_inf_cancel_left, himp_inf_cancel_right, himp_le_of_right_le, hnot_le_left, hnot_le_right, top_sdiff, disjoint_sdiff_left, disjoint_sdiff_right, le_compl_left, le_compl_right, le_sdiff_of_le_left, sdiff_eq_left, sdiff_eq_right, sup_sdiff_cancel_left, sup_sdiff_cancel_right, sdiff_le_iff, le_himp_iff, himp_bot, compl_eq, eq_compl, eq_hnot, hnot_eq, codisjoint_hnot_left, codisjoint_hnot_right, disjoint_compl_left, disjoint_compl_right, bot_eq, compl_eq, himp_eq, hnot_eq, inf_eq, sdiff_eq, sup_eq, top_eq, himp_apply, himp_def, hnot_apply, hnot_def, bot_himp, bot_sdiff, codisjoint_hnot_hnot_left_iff, codisjoint_hnot_hnot_right_iff, codisjoint_hnot_left, codisjoint_hnot_right, compl_anti, compl_bot, compl_compl_compl, compl_compl_himp_distrib, compl_compl_inf_distrib, compl_iff_not, compl_inf_eq_bot, compl_inf_self, compl_le_compl, compl_le_himp, compl_le_hnot, compl_ne_self, compl_sup, compl_sup_compl_le, compl_sup_distrib, compl_sup_le_himp, compl_top, compl_unique, disjoint_compl_compl_left_iff, disjoint_compl_compl_right_iff, disjoint_compl_left, disjoint_compl_right, fst_compl, fst_himp, fst_hnot, fst_sdiff, gc_inf_himp, gc_sdiff_sup, himp_bot, himp_compl, himp_compl_comm, himp_eq_himp_iff, himp_eq_top_iff, himp_himp, himp_idem, himp_iff_imp, himp_inf_distrib, himp_inf_himp_cancel, himp_inf_himp_inf_le, himp_inf_le, himp_inf_self, himp_le_himp, himp_le_himp_himp_himp, himp_le_himp_left, himp_le_himp_right, himp_left_comm, himp_ne_himp_iff, himp_self, himp_top, himp_triangle, hnot_anti, hnot_bot, hnot_hnot_hnot, hnot_hnot_le, hnot_hnot_sdiff_distrib, hnot_hnot_sup_distrib, hnot_inf_distrib, hnot_le_comm, hnot_le_hnot, hnot_le_iff_codisjoint_left, hnot_le_iff_codisjoint_right, hnot_sdiff, hnot_sdiff_comm, hnot_sup_self, hnot_top, inf_compl_eq_bot, inf_compl_self, inf_himp, inf_himp_le, inf_sdiff_left, inf_sdiff_right, inf_sdiff_sup_left, inf_sdiff_sup_right, le_compl_comm, le_compl_compl, le_compl_iff_disjoint_left, le_compl_iff_disjoint_right, le_compl_iff_le_compl, le_compl_of_le_compl, le_compl_self, le_himp, le_himp_comm, le_himp_himp, le_himp_iff, le_himp_iff', le_himp_iff_left, le_hnot_inf_hnot, le_sdiff_sup, le_sup_sdiff, le_sup_sdiff_sup_sdiff, lt_compl_self, ne_compl_self, ofDual_compl, ofDual_himp, ofDual_hnot, sdiff_bot, sdiff_eq_bot_iff, sdiff_eq_sdiff_iff, sdiff_idem, sdiff_inf, sdiff_inf_distrib, sdiff_inf_self_left, sdiff_inf_self_right, sdiff_le, sdiff_le_comm, sdiff_le_hnot, sdiff_le_iff, sdiff_le_iff', sdiff_le_iff_left, sdiff_le_inf_hnot, sdiff_le_sdiff, sdiff_le_sdiff_left, sdiff_le_sdiff_of_sup_le_sup_left, sdiff_le_sdiff_of_sup_le_sup_right, sdiff_le_sdiff_right, sdiff_ne_sdiff_iff, sdiff_right_comm, sdiff_sdiff, sdiff_sdiff_comm, sdiff_sdiff_le, sdiff_sdiff_left, sdiff_sdiff_sdiff_le_sdiff, sdiff_sdiff_self, sdiff_self, sdiff_sup_cancel, sdiff_sup_sdiff_cancel, sdiff_sup_sdiff_cancel', sdiff_sup_self, sdiff_top, sdiff_triangle, snd_compl, snd_himp, snd_hnot, snd_sdiff, sup_compl_le_himp, sup_himp_distrib, sup_himp_self_left, sup_himp_self_right, sup_hnot_self, sup_le_of_le_sdiff_left, sup_le_of_le_sdiff_right, sup_sdiff, sup_sdiff_cancel', sup_sdiff_cancel_right, sup_sdiff_distrib, sup_sdiff_eq_sup, sup_sdiff_left, sup_sdiff_left_self, sup_sdiff_right, sup_sdiff_right_self, sup_sdiff_self, sup_sdiff_self_left, sup_sdiff_self_right, toDual_compl, toDual_hnot, toDual_sdiff, top_himp, top_sdiff'	206
Total	265

BiheytingAlgebra

Definitions

Name	Category	Theorems
toCoheytingAlgebra 📖	CompOp	362 math math: Set.pairwiseDisjoint_range_iff, BooleanSubalgebra.mem_toSublattice, map_symmDiff', BoolAlg.coe_id, Set.pairwise_disjoint_Ioc_zpow, codisjoint_iff_compl_le_right, Set.pairwise_disjoint_Ioo_add_zsmul, Set.inter_symmDiff_distrib_left, Set.functorToTypes_obj, compl_symmDiff_self, Set.Finite.inf_of_right, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, Sym2.disjoint_diagSet_fromRel, Set.disjoint_compl_left_iff_subset, ofBoolRing_sub, bihimp_left_involutive, BiheytingHom.map_sdiff', Set.pairwise_disjoint_Ico_zsmul, WithBot.orderIsoPUnitSumLex_symm_inl, bihimp_bihimp_cancel_right, bihimp_eq_left, symmDiff_eq', Set.pairwise_disjoint_Ioo_mul_zpow, sup_inf_inf_compl, BooleanSubalgebra.map_map, Set.sdiff_singleton_wcovBy, Set.image_symmDiff, codisjoint_bihimp_sup, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, toBoolRing_inf, compl_inf, symmDiff_compl_self, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, Set.disjoint_of_subset_iff_left_eq_empty, inf_himp_bihimp, SetRel.core_mono, BoolAlg.ext_iff, Finset.compl_inf, Set.toFinset_symmDiff, WithBot.orderIsoPUnitSumLex_symm_inr, Order.Ideal.IsProper.notMem_or_compl_notMem, symmDiff_top, Set.isCompl_range_some_none, Set.indicator_symmDiff, pairwise_disjoint_fiber, Finset.compl_sup, Finset.inclusion_exclusion_card_inf_compl, bihimp_right_surjective, ofBoolAlg_inf, Set.symmDiff_def, Set.covBy_iff_exists_sdiff_singleton, instWellFoundedLTSubtypeSetFinite, disjoint_compl_right_iff, SetRel.prod_comp_prod, codisjoint_iff_compl_le_left, Set.disjoint_image_left, Set.sdiff_singleton_covBy, BooleanSubalgebra.inf_mem, bihimp_himp_left, Types.monoOverEquivalenceSet_inverse_map, BoolAlg.hasForgetToBoolRing_forget₂_map, top_symmDiff, BiheytingHom.toFun_eq_coe_aux, Set.pairwise_disjoint_Ioc_zsmul, isCoatom_compl, bihimp_eq_right, Set.subset_compl_iff_disjoint_right, BooleanSubalgebra.subtype_comp_inclusion, boolRingCatEquivBoolAlg_functor, Set.mem_symmDiff, BooleanSubalgebra.sup_mem, BoolAlg.ofHom_comp, compl_symmDiff, BooleanSubalgebra.mem_comap, SetRel.image_core_gc, Set.disjoint_sdiff_inter, ofBoolRing_add, Set.pairwise_disjoint_Ioo_add_intCast, Set.covBy_insert, compl_lt_self, BooleanSubalgebra.bot_mem', HasSubset.Subset.disjoint_compl_right, disjoint_of_sSup_disjoint, himp_bihimp_left, bihimp_left_comm, BooleanSubalgebra.coe_map, Finset.inf_himp_right, SimpleGraph.edgeSet_eq_iff, Set.pairwise_disjoint_Ioc_add_zsmul, BoolAlg.hom_id, WithTop.orderIsoSumLexPUnit_toLex, Set.disjoint_powerset_insert, Set.disjoint_toFinset, bihimp_left_surjective, bihimp_le_iff_left, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, BoolAlg.hasForgetToHeytAlg_forget₂_map, WithTop.orderIsoSumLexPUnit_symm_inl, Set.offDiag_mono, bihimp_le_iff_right, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, BooleanSubalgebra.mk_inf_mk, SimpleGraph.disjoint_edgeSet, iSup_eq_top, bihimp_bihimp_self, Finset.inclusion_exclusion_sum_inf_compl, FinBoolAlg.forgetToFinPartOrdFaithful, compl_image_latticeClosure, toBoolAlg_add, Set.union_symmDiff_subset, BooleanSubalgebra.subtype_injective, ofBoolAlg_sup, Set.pairwise_disjoint_Ico_add_intCast, Finset.isCoatom_compl_singleton, BooleanSubalgebra.apply_coe_mem_map, Set.subset_diff, Int.isCompl_even_odd, himp_le, compl_lt_compl_iff_lt, Order.Ideal.isPrime_iff_mem_or_compl_mem, toBoolAlg_add_add_mul, Set.Finite.toFinset_symmDiff, Finset.diffs_compls_eq_infs, BiheytingHomClass.toLatticeHomClass, Set.nsmul_right_monotone, compl_image_latticeClosure_eq_of_compl_image_eq_self, symmDiff_eq, Set.mulIndicator_symmDiff, WithTop.orderIsoSumLexPUnit_top, OrderIso.compl_symm_apply, ofBoolRing_le_ofBoolRing_iff, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, BooleanSubalgebra.mk_sup_mk, himp_le_left, Set.disjoint_prod, Finset.inf_sdiff_right, bihimp_eq, BooleanSubalgebra.coe_inclusion, BooleanSubalgebra.comap_id, Set.indicator_eq_zero', bihimp_right_inj, bihimp_right_comm, Set.disjoint_image_iff, Set.disjoint_pi, Set.indicator_eq_zero, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, Set.empty_covBy_singleton, Coheyting.boundary_eq_bot, disjoint_of_sSup_disjoint_of_le_of_le, bihimp_iff_iff, BooleanSubalgebra.latticeClosure_subset_closure, BooleanAlgebra.le_iff_atom_le_imp, ofBoolAlg_symmDiff, BiheytingHom.toFun_eq_coe, Set.pow_right_monotone, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, Set.apply_indicator_symmDiff, BooleanSubalgebra.infClosed, BooleanSubalgebra.closure_latticeClosure, RingHom.asBoolAlg_id, compl_le_self, Set.disjoint_compl_right_iff_subset, BoolAlg.hom_comp, Set.pairwise_disjoint_Ioo_zpow, Set.Finite.inf_of_left, gc_Ici_sInf, Set.disjoint_image_image, Set.symmDiff_subset_union, BooleanSubalgebra.mem_map_of_mem, eq_compl_iff_isCompl, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, BooleanSubalgebra.val_inf, RingHom.asBoolAlg_comp, BooleanSubalgebra.subtype_apply, Set.zero_mem_neg_add_iff, Set.pairwise_disjoint_Ioc_intCast, BooleanSubalgebra.inclusion_injective, Set.subset_compl_iff_disjoint_left, Types.monoOverEquivalenceSet_functor_map, BoolAlg.ofHom_id, BoolAlg.dual_map, disjoint_compl_left_iff, Set.pairwise_disjoint_Ioo_zsmul, CategoryTheory.Limits.Types.isPushout_of_bicartSq, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, BiheytingHomClass.toCoheytingHomClass, boolRingCatEquivBoolAlg_inverse, compl_symmDiff_compl, SimpleGraph.fromEdgeSet_disjoint, Finset.compls_sups, BoolAlg.coe_comp, SetRel.image_mono, Function.Injective.image_strictMono, BoundedLatticeHom.asBoolRing_apply, Set.disjoint_image_right, Types.monoOverEquivalenceSet_functor_obj, BooleanSubalgebra.val_sup, BoolRing.hasForgetToBoolAlg_forget₂_map, himp_bihimp_right, Function.mulSupport_disjoint_iff, Booleanisation.liftLatticeHom_injective, BoolAlg.hom_inv_apply, MeasureTheory.preVariation.sum_le, Set.pairwise_disjoint_Ioc_add_intCast, bihimp_right_involutive, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, Set.Finite.symmDiff_congr, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion', Set.inter_symmDiff_distrib_right, bihimp_eq_inf, SetRel.preimage_mono, BooleanSubalgebra.mem_map, Finset.compls_infs, Finset.coe_symmDiff, Set.mulIndicator_eq_one', Function.support_disjoint_iff, Set.isCompl_range_inl_range_inr, Set.one_notMem_inv_mul_iff, Set.preimage_eq_empty_iff, BoolAlg.comp_apply, Finset.mem_inf, PUnit.top_eq, TopologicalSpace.Clopens.surjective_finset_sup_prod, WithBot.orderIsoPUnitSumLex_toLex, ofBoolRing_mul, Set.disjoint_image_inl_image_inr, compl_antitone, Set.disjoint_sdiff_left, compl_strictAnti, gc_sSup_Iic, sdiff_compl, Set.pairwise_disjoint_Ico_zpow, BoundedLatticeHom.asBoolRing_id, BiheytingHom.map_himp', Set.disjoint_preimage_iff, finBoolAlg_dual_comp_forget_to_finBddDistLat, Set.apply_mulIndicator_symmDiff, Finset.infs_compls_eq_diffs, TopologicalSpace.Clopens.coe_finset_sup, Finset.sup_sdiff_left, SimpleGraph.IsCompleteBetween.disjoint, Set.disjoint_sdiff_right, symmDiff_eq_Xor', Set.zero_notMem_sub_iff, MeasureTheory.preVariation.exists_Finpartition_sum_ge, Set.one_notMem_div_iff, bihimp_left_inj, bihimp_left_injective, BoundedLatticeHom.asBoolRing_comp, MeasureTheory.preVariation.exists_Finpartition_sum_gt, OrderIso.asBoolAlgAsBoolRing_apply, sSup_eq_top, Set.Finite.disjoint_toFinset, Finset.compls_infs_eq_diffs, bihimp_bihimp_cancel_left, Set.pairwiseDisjoint_range_singleton, symmDiff_symmDiff_right', Set.Finite.symmDiff, Set.disjoint_diagonal_offDiag, SetRel.gc_leftDual_rightDual, BooleanSubalgebra.mem_carrier, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, compl_le_compl_iff_le, Set.symmDiff_eq_empty, OrderIso.compl_apply, Set.mulIndicator_eq_one, compl_le_hnot, BooleanSubalgebra.coe_subtype, Types.monoOverEquivalenceSet_inverse_obj, BooleanSubalgebra.inclusion_rfl, maximal_subtype, Finset.sup_himp_right, compl_eq_iff_isCompl, symmDiff_eq_top, Set.one_mem_div_iff, Set.pairwise_disjoint_Ico_intCast, SimpleGraph.disjoint_fromEdgeSet, PUnit.sup_eq, Set.pairwiseDisjoint_fiber, WithTop.orderIsoSumLexPUnit_symm_inr, instWellFoundedGTUnit, Finset.isCoatom_iff, bihimp_bihimp_bihimp_comm, Set.zero_notMem_neg_add_iff, Set.disjoint_image_inl_range_inr, BooleanSubalgebra.coe_comap, subsingleton_setOf_mem_iff_pairwise_disjoint, Set.pairwiseDisjoint_image_right_iff, Finset.compl_truncatedInf, BoolAlg.inv_hom_apply, Types.monoOverEquivalenceSet_unitIso, boolAlg_dual_comp_forget_to_bddDistLat, codisjoint_himp_self_left, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, BooleanSubalgebra.mem_map_equiv, FinBoolAlg.forgetToBoolAlg_full, Finset.inf_sdiff_left, Set.symmDiff_nonempty, compl_le_iff_compl_le, Set.preimage_symmDiff, BooleanSubalgebra.inclusion_apply, Set.functorToTypes_map, Set.Finite.sup, Nat.isCompl_even_odd, Set.subset_image_symmDiff, Set.zero_mem_sub_iff, BooleanSubalgebra.map_id, compl_bihimp_compl, Set.pairwiseDisjoint_image_left_iff, Set.monotone_image, Set.wcovBy_insert, minimal_subtype, bihimp_eq', Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, PUnit.inf_eq, Set.covBy_iff_exists_insert, Set.disjoint_range_inl_image_inr, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, Set.pairwise_disjoint_Ico_add_zsmul, bihimp_isAssociative, BooleanSubalgebra.supClosed, compl_bihimp, MeasureTheory.preVariation.sum_le_preVariationFun_of_subset, codisjoint_himp_self_right, Types.monoOverEquivalenceSet_counitIso, Order.Ideal.IsPrime.isMaximal, FinBoolAlg.dual_map, OrderIso.asBoolAlgAsBoolRing_symm_apply, Finset.sup_himp_left, iSup₂_eq_top, BoolAlg.id_apply, Pi.mulSupport_mulSingle_disjoint, Set.prod_subset_compl_diagonal_iff_disjoint, BooleanAlgebra.eq_iff_atom_le_iff, toBoolRing_symmDiff, bihimp_himp_right, bihimp_assoc, Set.symmDiff_union_subset, Set.pairwise_disjoint_Ioo_intCast, FinBoolAlg.forgetToBoolAlgFaithful, isAtom_compl, toBoolAlg_mul, Finset.compl_truncatedSup, Finset.card_truncatedSup_union_add_card_truncatedSup_infs, Order.Ideal.IsPrime.mem_or_compl_mem, Function.disjoint_support_iff, bihimp_eq_bot, Set.union_symmDiff_union_subset, Set.one_mem_inv_mul_iff, BooleanSubalgebra.comap_comap, WithBot.orderIsoPUnitSumLex_bot, BoolAlg.ofHom_apply, BoolAlg.forget_map, Set.disjoint_univ_pi, RingHom.asBoolAlg_toFun, bihimp_right_injective, Set.pairwiseDisjoint_singleton_iff_injOn
toHNot 📖	CompOp	5 math math: SimpleGraph.Finsubgraph.coe_hnot, hnot_eq_compl, PUnit.hnot_eq, compl_le_hnot, top_sdiff
toHeytingAlgebra 📖	CompOp	123 math math: Set.pairwiseDisjoint_range_iff, Set.pairwise_disjoint_Ioc_zpow, Set.pairwise_disjoint_Ioo_add_zsmul, BiheytingHomClass.toHeytingHomClass, Sym2.disjoint_diagSet_fromRel, Set.disjoint_compl_left_iff_subset, Set.pairwise_disjoint_Ico_zsmul, Set.pairwise_disjoint_Ioo_mul_zpow, PUnit.bot_eq, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, Set.disjoint_of_subset_iff_left_eq_empty, Finset.compl_inf, pairwise_disjoint_fiber, Finset.compl_sup, disjoint_compl_right_iff, SetRel.prod_comp_prod, Set.disjoint_image_left, Set.pairwise_disjoint_Ioc_zsmul, isCoatom_compl, Set.subset_compl_iff_disjoint_right, Set.disjoint_sdiff_inter, Set.pairwise_disjoint_Ioo_add_intCast, HasSubset.Subset.disjoint_compl_right, disjoint_of_sSup_disjoint, Finset.inf_himp_right, SimpleGraph.edgeSet_eq_iff, Set.pairwise_disjoint_Ioc_add_zsmul, Set.disjoint_powerset_insert, Set.disjoint_toFinset, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, BoolAlg.hasForgetToHeytAlg_forget₂_map, TopologicalSpace.Clopens.coe_disjoint, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, SimpleGraph.disjoint_edgeSet, Set.pairwise_disjoint_Ico_add_intCast, Set.subset_diff, Set.disjoint_prod, Set.indicator_eq_zero', Set.disjoint_image_iff, Set.disjoint_pi, Set.indicator_eq_zero, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, disjoint_of_sSup_disjoint_of_le_of_le, BooleanSubalgebra.mem_closure_iff_sup_sdiff, Set.disjoint_compl_right_iff_subset, Set.pairwise_disjoint_Ioo_zpow, Set.disjoint_image_image, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, Set.zero_mem_neg_add_iff, Set.pairwise_disjoint_Ioc_intCast, Set.subset_compl_iff_disjoint_left, disjoint_compl_left_iff, Set.pairwise_disjoint_Ioo_zsmul, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, SimpleGraph.fromEdgeSet_disjoint, Set.disjoint_image_right, Function.mulSupport_disjoint_iff, MeasureTheory.preVariation.sum_le, Set.pairwise_disjoint_Ioc_add_intCast, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion', Set.mulIndicator_eq_one', Function.support_disjoint_iff, Set.one_notMem_inv_mul_iff, Set.preimage_eq_empty_iff, TopologicalSpace.Clopens.surjective_finset_sup_prod, Set.disjoint_image_inl_image_inr, Set.disjoint_sdiff_left, Set.pairwise_disjoint_Ico_zpow, BiheytingHom.map_himp', Set.disjoint_preimage_iff, TopologicalSpace.Clopens.coe_finset_sup, Finset.sup_sdiff_left, SimpleGraph.IsCompleteBetween.disjoint, Set.disjoint_sdiff_right, Set.zero_notMem_sub_iff, MeasureTheory.preVariation.exists_Finpartition_sum_ge, Set.one_notMem_div_iff, MeasureTheory.preVariation.exists_Finpartition_sum_gt, PUnit.himp_eq, Set.Finite.disjoint_toFinset, Set.pairwiseDisjoint_range_singleton, Set.disjoint_diagonal_offDiag, Set.mulIndicator_eq_one, compl_le_hnot, Finset.sup_himp_right, Set.one_mem_div_iff, Set.pairwise_disjoint_Ico_intCast, SimpleGraph.disjoint_fromEdgeSet, Set.pairwiseDisjoint_fiber, iInf_eq_bot, Set.zero_notMem_neg_add_iff, Set.disjoint_image_inl_range_inr, subsingleton_setOf_mem_iff_pairwise_disjoint, Set.pairwiseDisjoint_image_right_iff, iInf₂_eq_bot, ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, Finset.inf_sdiff_left, PUnit.compl_eq, Set.zero_mem_sub_iff, Set.pairwiseDisjoint_image_left_iff, Set.disjoint_range_inl_image_inr, top_sdiff, Set.pairwise_disjoint_Ico_add_zsmul, MeasureTheory.preVariation.sum_le_preVariationFun_of_subset, Finset.sup_himp_left, sdiff_le_iff, Pi.mulSupport_mulSingle_disjoint, Set.prod_subset_compl_diagonal_iff_disjoint, IsCoatom.of_compl, sInf_eq_bot, IsCoatom.compl, Set.pairwise_disjoint_Ioo_intCast, TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, isAtom_compl, Function.disjoint_support_iff, BiheytingHomClass.map_himp, Set.one_mem_inv_mul_iff, Set.disjoint_univ_pi, Set.pairwiseDisjoint_singleton_iff_injOn
toSDiff 📖	CompOp	6 math math: BiheytingHomClass.map_sdiff, BiheytingHom.map_sdiff', SimpleGraph.Finsubgraph.coe_sdiff, PUnit.sdiff_eq, top_sdiff, sdiff_le_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sdiff_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra toHeytingAlgebra toSDiff SemilatticeSup.toMax	—	—
top_sdiff 📖	mathematical	—	toSDiff Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra toHeytingAlgebra GeneralizedHeytingAlgebra.toOrderTop HNot.hnot toHNot	—	—

Codisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
himp_eq_left 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	himp_eq_right symm
himp_eq_right 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	top_himp eq_top sup_himp_self_left
himp_inf_cancel_left 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeInf.toMin	—	himp_inf_distrib himp_self inf_top_eq himp_eq_right
himp_inf_cancel_right 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeInf.toMin	—	himp_inf_distrib himp_self top_inf_eq himp_eq_left
himp_le_of_right_le 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop Preorder.toLE PartialOrder.toPreorder	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	LE.le.trans_eq himp_le_himp_left himp_eq_right
hnot_le_left 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop	Preorder.toLE PartialOrder.toPreorder HNot.hnot CoheytingAlgebra.toHNot	—	hnot_le_iff_codisjoint_left
hnot_le_right 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop	Preorder.toLE PartialOrder.toPreorder HNot.hnot CoheytingAlgebra.toHNot	—	hnot_le_iff_codisjoint_right

CoheytingAlgebra

Definitions

Name	Category	Theorems
ofHNot 📖	CompOp	—
ofSDiff 📖	CompOp	—
toBoundedOrder 📖	CompOp	6 math math: Coheyting.boundary_top, hnot_top, hnot_bot, sdiff_top, CoheytingHomClass.toBoundedLatticeHomClass, Coheyting.boundary_bot
toDistribLattice 📖	CompOp	—
toGeneralizedCoheytingAlgebra 📖	CompOp	428 math math: Set.pairwiseDisjoint_range_iff, BooleanSubalgebra.mem_toSublattice, map_symmDiff', BoolAlg.coe_id, Set.pairwise_disjoint_Ioc_zpow, codisjoint_iff_compl_le_right, Set.pairwise_disjoint_Ioo_add_zsmul, Set.inter_symmDiff_distrib_left, Set.functorToTypes_obj, compl_symmDiff_self, Set.Finite.inf_of_right, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, Sym2.disjoint_diagSet_fromRel, Set.disjoint_compl_left_iff_subset, ofBoolRing_sub, bihimp_left_involutive, AlgebraicGeometry.Scheme.support_nilradical, BiheytingHom.map_sdiff', Set.pairwise_disjoint_Ico_zsmul, WithBot.orderIsoPUnitSumLex_symm_inl, bihimp_bihimp_cancel_right, bihimp_eq_left, symmDiff_eq', Set.pairwise_disjoint_Ioo_mul_zpow, sup_inf_inf_compl, BooleanSubalgebra.map_map, Set.sdiff_singleton_wcovBy, Set.image_symmDiff, codisjoint_bihimp_sup, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, toBoolRing_inf, compl_inf, symmDiff_compl_self, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, Set.disjoint_of_subset_iff_left_eq_empty, inf_himp_bihimp, SetRel.core_mono, BoolAlg.ext_iff, Coheyting.boundary_top, Finset.compl_inf, hnot_le_iff_codisjoint_left, Set.toFinset_symmDiff, WithBot.orderIsoPUnitSumLex_symm_inr, Order.Ideal.IsProper.notMem_or_compl_notMem, Coheyting.boundary_le_hnot, symmDiff_top, Set.isCompl_range_some_none, Coheyting.hnot_boundary, hnot_symmDiff_self, Set.indicator_symmDiff, pairwise_disjoint_fiber, Finset.compl_sup, bihimp_right_surjective, Coheyting.hnot_eq_top_iff_exists_boundary, hnot_hnot_le, ofBoolAlg_inf, Set.symmDiff_def, Set.covBy_iff_exists_sdiff_singleton, instWellFoundedLTSubtypeSetFinite, disjoint_compl_right_iff, symmDiff_top', SetRel.prod_comp_prod, codisjoint_iff_compl_le_left, Set.disjoint_image_left, Set.sdiff_singleton_covBy, BooleanSubalgebra.inf_mem, bihimp_himp_left, Types.monoOverEquivalenceSet_inverse_map, BoolAlg.hasForgetToBoolRing_forget₂_map, top_symmDiff, codisjoint_hnot_right, Fin.top_eq_last, BiheytingHom.toFun_eq_coe_aux, Set.pairwise_disjoint_Ioc_zsmul, isCoatom_compl, bihimp_eq_right, Set.subset_compl_iff_disjoint_right, BooleanSubalgebra.subtype_comp_inclusion, boolRingCatEquivBoolAlg_functor, le_hnot_inf_hnot, sdiff_le_hnot, Set.mem_symmDiff, BooleanSubalgebra.sup_mem, BoolAlg.ofHom_comp, compl_symmDiff, BooleanSubalgebra.mem_comap, SetRel.image_core_gc, Set.disjoint_sdiff_inter, ofBoolRing_add, Fin.rev_top, CoheytingHom.toFun_eq_coe_aux, Set.pairwise_disjoint_Ioo_add_intCast, toDual_sdiff, liminf_eq_top, Set.covBy_insert, ofDual_himp, compl_lt_self, BooleanSubalgebra.bot_mem', HasSubset.Subset.disjoint_compl_right, Fin.top_eq_zero, disjoint_of_sSup_disjoint, himp_bihimp_left, bihimp_left_comm, BooleanSubalgebra.coe_map, Finset.inf_himp_right, SimpleGraph.edgeSet_eq_iff, Set.pairwise_disjoint_Ioc_add_zsmul, BoolAlg.hom_id, WithTop.orderIsoSumLexPUnit_toLex, Set.disjoint_powerset_insert, Set.disjoint_toFinset, bihimp_left_surjective, bihimp_le_iff_left, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, BoolAlg.hasForgetToHeytAlg_forget₂_map, WithTop.orderIsoSumLexPUnit_symm_inl, Coheyting.hnot_hnot_sup_boundary, Set.offDiag_mono, bihimp_le_iff_right, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, BooleanSubalgebra.mk_inf_mk, SimpleGraph.disjoint_edgeSet, iSup_eq_top, bihimp_bihimp_self, iSup_sdiff_eq, CoheytingHomClass.map_top, FinBoolAlg.forgetToFinPartOrdFaithful, compl_image_latticeClosure, toBoolAlg_add, CoheytingHomClass.map_sdiff, Coheyting.boundary_sup_le, Set.union_symmDiff_subset, CoheytingHomClass.toLatticeHomClass, sup_hnot_self, BooleanSubalgebra.subtype_injective, ofBoolAlg_sup, Set.pairwise_disjoint_Ico_add_intCast, BooleanSubalgebra.apply_coe_mem_map, Set.subset_diff, Int.isCompl_even_odd, hnot_top, himp_le, compl_lt_compl_iff_lt, hnot_sdiff_comm, Order.Ideal.isPrime_iff_mem_or_compl_mem, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, toBoolAlg_add_add_mul, Set.Finite.toFinset_symmDiff, Finset.diffs_compls_eq_infs, BiheytingHomClass.toLatticeHomClass, Set.nsmul_right_monotone, compl_image_latticeClosure_eq_of_compl_image_eq_self, CoheytingHom.map_top', symmDiff_eq, Set.mulIndicator_symmDiff, hnot_bot, WithTop.orderIsoSumLexPUnit_top, OrderIso.compl_symm_apply, ofBoolRing_le_ofBoolRing_iff, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, BooleanSubalgebra.mk_sup_mk, himp_le_left, Set.disjoint_prod, Finset.inf_sdiff_right, Coheyting.boundary_inf, bihimp_eq, BooleanSubalgebra.coe_inclusion, BooleanSubalgebra.comap_id, Set.indicator_eq_zero', bihimp_right_inj, bihimp_right_comm, Set.disjoint_image_iff, Set.disjoint_pi, Set.indicator_eq_zero, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, Set.empty_covBy_singleton, disjoint_of_sSup_disjoint_of_le_of_le, bihimp_iff_iff, BooleanSubalgebra.latticeClosure_subset_closure, sdiff_le_inf_hnot, BooleanAlgebra.le_iff_atom_le_imp, ofBoolAlg_symmDiff, BiheytingHom.toFun_eq_coe, Set.pow_right_monotone, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, Set.apply_indicator_symmDiff, BooleanSubalgebra.infClosed, Coheyting.inf_hnot_self, BooleanSubalgebra.closure_latticeClosure, RingHom.asBoolAlg_id, compl_le_self, Set.disjoint_compl_right_iff_subset, BoolAlg.hom_comp, Set.pairwise_disjoint_Ioo_zpow, Set.Finite.inf_of_left, gc_Ici_sInf, Set.disjoint_image_image, Set.symmDiff_subset_union, BooleanSubalgebra.mem_map_of_mem, eq_compl_iff_isCompl, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, BooleanSubalgebra.val_inf, RingHom.asBoolAlg_comp, hnot_inf_distrib, CoheytingHom.map_sdiff', Coheyting.boundary_inf_le, codisjoint_hnot_left, sdiff_eq_sInf, BooleanSubalgebra.subtype_apply, Set.zero_mem_neg_add_iff, Set.pairwise_disjoint_Ioc_intCast, BooleanSubalgebra.inclusion_injective, Set.subset_compl_iff_disjoint_left, le_sdiff_iff, Types.monoOverEquivalenceSet_functor_map, BoolAlg.ofHom_id, BoolAlg.dual_map, disjoint_compl_left_iff, Set.pairwise_disjoint_Ioo_zsmul, CategoryTheory.Limits.Types.isPushout_of_bicartSq, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, Coheyting.boundary_hnot_le, boolRingCatEquivBoolAlg_inverse, compl_symmDiff_compl, Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left, SimpleGraph.fromEdgeSet_disjoint, Finset.compls_sups, BoolAlg.coe_comp, SetRel.image_mono, Function.Injective.image_strictMono, BoundedLatticeHom.asBoolRing_apply, Set.disjoint_image_right, Types.monoOverEquivalenceSet_functor_obj, BooleanSubalgebra.val_sup, BoolRing.hasForgetToBoolAlg_forget₂_map, himp_bihimp_right, Function.mulSupport_disjoint_iff, Booleanisation.liftLatticeHom_injective, BoolAlg.hom_inv_apply, MeasureTheory.preVariation.sum_le, Set.pairwise_disjoint_Ioc_add_intCast, bihimp_right_involutive, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, Set.Finite.symmDiff_congr, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion', hnot_hnot_sdiff_distrib, Set.inter_symmDiff_distrib_right, bihimp_eq_inf, SetRel.preimage_mono, BooleanSubalgebra.mem_map, Finset.compls_infs, Finset.coe_symmDiff, Set.mulIndicator_eq_one', Function.support_disjoint_iff, Set.isCompl_range_inl_range_inr, Coheyting.boundary_le, Set.one_notMem_inv_mul_iff, Fin.cast_top, Set.preimage_eq_empty_iff, BoolAlg.comp_apply, PUnit.top_eq, isLeast_hnot, TopologicalSpace.Clopens.surjective_finset_sup_prod, WithBot.orderIsoPUnitSumLex_toLex, ofBoolRing_mul, Set.disjoint_image_inl_image_inr, compl_antitone, Set.disjoint_sdiff_left, compl_strictAnti, gc_sSup_Iic, sdiff_compl, Set.pairwise_disjoint_Ico_zpow, BoundedLatticeHom.asBoolRing_id, BiheytingHom.map_himp', Set.disjoint_preimage_iff, finBoolAlg_dual_comp_forget_to_finBddDistLat, Set.apply_mulIndicator_symmDiff, Finset.infs_compls_eq_diffs, TopologicalSpace.Clopens.coe_finset_sup, Finset.sup_sdiff_left, SimpleGraph.IsCompleteBetween.disjoint, Set.disjoint_sdiff_right, codisjoint_hnot_hnot_left_iff, symmDiff_eq_Xor', Set.zero_notMem_sub_iff, MeasureTheory.preVariation.exists_Finpartition_sum_ge, Set.one_notMem_div_iff, bihimp_left_inj, bihimp_left_injective, BoundedLatticeHom.asBoolRing_comp, MeasureTheory.preVariation.exists_Finpartition_sum_gt, OrderIso.asBoolAlgAsBoolRing_apply, sSup_eq_top, Set.Finite.disjoint_toFinset, Finset.compls_infs_eq_diffs, bihimp_bihimp_cancel_left, Set.pairwiseDisjoint_range_singleton, symmDiff_symmDiff_right', Fin.rev_zero_eq_top, Set.Finite.symmDiff, Set.disjoint_diagonal_offDiag, SetRel.gc_leftDual_rightDual, hnot_sdiff, BooleanSubalgebra.mem_carrier, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, compl_le_compl_iff_le, Set.symmDiff_eq_empty, OrderIso.compl_apply, CoheytingHom.toFun_eq_coe, symmDiff_hnot_self, Set.mulIndicator_eq_one, compl_le_hnot, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, sdiff_top, BooleanSubalgebra.coe_subtype, CoheytingHomClass.toBoundedLatticeHomClass, Types.monoOverEquivalenceSet_inverse_obj, BooleanSubalgebra.inclusion_rfl, hnot_sup_self, maximal_subtype, Finset.sup_himp_right, compl_eq_iff_isCompl, symmDiff_eq_top, Set.one_mem_div_iff, Fin.range_natAdd_eq_Ioi, Set.pairwise_disjoint_Ico_intCast, SimpleGraph.disjoint_fromEdgeSet, PUnit.sup_eq, Set.pairwiseDisjoint_fiber, WithTop.orderIsoSumLexPUnit_symm_inr, instWellFoundedGTUnit, bihimp_bihimp_bihimp_comm, Set.zero_notMem_neg_add_iff, Set.disjoint_image_inl_range_inr, BooleanSubalgebra.coe_comap, subsingleton_setOf_mem_iff_pairwise_disjoint, Set.pairwiseDisjoint_image_right_iff, Finset.compl_truncatedInf, BoolAlg.inv_hom_apply, Types.monoOverEquivalenceSet_unitIso, boolAlg_dual_comp_forget_to_bddDistLat, codisjoint_himp_self_left, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, BooleanSubalgebra.mem_map_equiv, FinBoolAlg.forgetToBoolAlg_full, Finset.inf_sdiff_left, Set.symmDiff_nonempty, compl_le_iff_compl_le, Set.preimage_symmDiff, BooleanSubalgebra.inclusion_apply, Set.functorToTypes_map, Set.Finite.sup, Nat.isCompl_even_odd, Set.subset_image_symmDiff, Set.zero_mem_sub_iff, BooleanSubalgebra.map_id, compl_bihimp_compl, Set.pairwiseDisjoint_image_left_iff, Set.monotone_image, Set.wcovBy_insert, hnot_anti, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, map_symmDiff, Fin.val_top, minimal_subtype, bihimp_eq', Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, hnot_le_comm, PUnit.inf_eq, Coheyting.boundary_sup_sup_boundary_inf, Set.covBy_iff_exists_insert, Set.disjoint_range_inl_image_inr, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, Set.pairwise_disjoint_Ico_add_zsmul, bihimp_isAssociative, top_symmDiff', top_sdiff', BooleanSubalgebra.supClosed, compl_bihimp, MeasureTheory.preVariation.sum_le_preVariationFun_of_subset, codisjoint_himp_self_right, hnot_hnot_sup_distrib, Types.monoOverEquivalenceSet_counitIso, Order.Ideal.IsPrime.isMaximal, FinBoolAlg.dual_map, OrderIso.asBoolAlgAsBoolRing_symm_apply, Finset.sup_himp_left, iSup₂_eq_top, BoolAlg.id_apply, Fin.zero_eq_top, Pi.mulSupport_mulSingle_disjoint, Set.prod_subset_compl_diagonal_iff_disjoint, hnot_le_iff_codisjoint_right, BooleanAlgebra.eq_iff_atom_le_iff, Fin.rev_bot, sdiff_iSup_eq, toBoolRing_symmDiff, bihimp_himp_right, bihimp_assoc, Set.symmDiff_union_subset, Coheyting.boundary_bot, Set.pairwise_disjoint_Ioo_intCast, FinBoolAlg.forgetToBoolAlgFaithful, Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right, isAtom_compl, toBoolAlg_mul, Finset.compl_truncatedSup, Order.Ideal.IsPrime.mem_or_compl_mem, Function.disjoint_support_iff, bihimp_eq_bot, Set.union_symmDiff_union_subset, codisjoint_hnot_hnot_right_iff, Set.one_mem_inv_mul_iff, BooleanSubalgebra.comap_comap, WithBot.orderIsoPUnitSumLex_bot, Fin.succ_top, BoolAlg.ofHom_apply, BoolAlg.forget_map, top_sdiff, Set.disjoint_univ_pi, RingHom.asBoolAlg_toFun, bihimp_right_injective, Set.pairwiseDisjoint_singleton_iff_injOn
toHNot 📖	CompOp	49 math math: hnot_le_iff_codisjoint_left, Coheyting.boundary_le_hnot, Coheyting.hnot_boundary, hnot_symmDiff_self, Coheyting.hnot_eq_top_iff_exists_boundary, hnot_hnot_le, symmDiff_top', ofDual_hnot, codisjoint_hnot_right, le_hnot_inf_hnot, sdiff_le_hnot, Codisjoint.hnot_le_left, map_hnot, Coheyting.hnot_hnot_sup_boundary, sup_hnot_self, hnot_top, hnot_sdiff_comm, toDual_compl, hnot_bot, ofDual_compl, Codisjoint.hnot_le_right, toDual_hnot, Coheyting.boundary_hnot_hnot, IsCompl.hnot_eq, sdiff_le_inf_hnot, hnot_eq_sInf_codisjoint, Coheyting.inf_hnot_self, hnot_inf_distrib, LE.le.codisjoint_hnot_right, codisjoint_hnot_left, IsCompl.eq_hnot, Coheyting.boundary_hnot_le, hnot_hnot_sdiff_distrib, hnot_hnot_hnot, isLeast_hnot, LE.le.codisjoint_hnot_left, codisjoint_hnot_hnot_left_iff, hnot_sdiff, symmDiff_hnot_self, hnot_sup_self, hnot_le_hnot, hnot_anti, hnot_le_comm, top_symmDiff', top_sdiff', hnot_hnot_sup_distrib, hnot_le_iff_codisjoint_right, codisjoint_hnot_hnot_right_iff, top_sdiff
toOrderTop 📖	CompOp	78 math math: codisjoint_iff_compl_le_right, AlgebraicGeometry.Scheme.support_nilradical, codisjoint_bihimp_sup, Coheyting.boundary_top, Finset.compl_inf, hnot_le_iff_codisjoint_left, Coheyting.hnot_boundary, hnot_symmDiff_self, IsCompl.symmDiff_eq_top, Finset.compl_sup, Finset.inclusion_exclusion_card_inf_compl, Coheyting.hnot_eq_top_iff_exists_boundary, symmDiff_top', codisjoint_iff_compl_le_left, Prop.isCoatom_iff, codisjoint_hnot_right, Fin.top_eq_last, isCoatom_compl, Fin.rev_top, liminf_eq_top, Fin.top_eq_zero, Finset.inf_himp_right, CompleteAtomicBooleanAlgebra.instIsCoatomistic, bihimp_le_iff_left, bihimp_le_iff_right, iSup_eq_top, CoheytingHomClass.map_top, Finset.inclusion_exclusion_sum_inf_compl, sup_hnot_self, Finset.isCoatom_compl_singleton, hnot_top, himp_le, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, CoheytingHom.map_top', hnot_bot, Finset.inf_sdiff_right, hnot_eq_sInf_codisjoint, LE.le.codisjoint_hnot_right, codisjoint_hnot_left, RestrictedProduct.isEmbedding_inclusion_top, bihimp_eq_inf, IsAtom.of_compl, Fin.cast_top, Finset.mem_inf, PUnit.top_eq, isLeast_hnot, LE.le.codisjoint_hnot_left, Finset.sup_sdiff_left, codisjoint_hnot_hnot_left_iff, sSup_eq_top, Fin.rev_zero_eq_top, symmDiff_hnot_self, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, sdiff_top, hnot_sup_self, Finset.sup_himp_right, Fin.range_natAdd_eq_Ioi, IsAtom.compl, Finset.isCoatom_iff, Finset.compl_truncatedInf, codisjoint_himp_self_left, Finset.inf_sdiff_left, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, Fin.val_top, UpperSet.codisjoint_prod, top_symmDiff', top_sdiff', codisjoint_himp_self_right, iSup₂_eq_top, Fin.zero_eq_top, hnot_le_iff_codisjoint_right, Fin.rev_bot, isAtom_compl, Finset.compl_truncatedSup, Finset.card_truncatedSup_union_add_card_truncatedSup_infs, codisjoint_hnot_hnot_right_iff, Fin.succ_top, top_sdiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
top_sdiff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff toGeneralizedCoheytingAlgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice toOrderTop HNot.hnot toHNot	—	—

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_sdiff_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	GeneralizedCoheytingAlgebra.toSDiff	—	mono_left sdiff_le
disjoint_sdiff_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	GeneralizedCoheytingAlgebra.toSDiff	—	mono_right sdiff_le
le_compl_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot	Preorder.toLE PartialOrder.toPreorder Compl.compl HeytingAlgebra.toCompl	—	le_compl_iff_disjoint_left
le_compl_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot	Preorder.toLE PartialOrder.toPreorder Compl.compl HeytingAlgebra.toCompl	—	le_compl_iff_disjoint_right
le_sdiff_of_le_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot Preorder.toLE PartialOrder.toPreorder	GeneralizedCoheytingAlgebra.toSDiff	—	LE.le.trans Eq.ge sdiff_eq_left sdiff_le_sdiff_right
sdiff_eq_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_bot eq_bot sdiff_inf_self_left
sdiff_eq_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_eq_left symm
sup_sdiff_cancel_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_sdiff sdiff_self bot_sup_eq sdiff_eq_right
sup_sdiff_cancel_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_sdiff sdiff_self sup_bot_eq sdiff_eq_left

Function.Injective

Definitions

Name	Category	Theorems
biheytingAlgebra 📖	CompOp	—
coheytingAlgebra 📖	CompOp	—
generalizedCoheytingAlgebra 📖	CompOp	—
generalizedHeytingAlgebra 📖	CompOp	—
heytingAlgebra 📖	CompOp	—

GeneralizedCoheytingAlgebra

Definitions

Name	Category	Theorems
toDistribLattice 📖	CompOp	—
toLattice 📖	CompOp	574 math math: Set.pairwiseDisjoint_range_iff, BooleanSubalgebra.mem_toSublattice, map_symmDiff', BoolAlg.coe_id, Set.pairwise_disjoint_Ioc_zpow, codisjoint_iff_compl_le_right, Pi.symmDiff_def, Set.pairwise_disjoint_Ioo_add_zsmul, Set.inter_symmDiff_distrib_left, Set.functorToTypes_obj, compl_symmDiff_self, Set.Finite.inf_of_right, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, Sym2.disjoint_diagSet_fromRel, Set.disjoint_compl_left_iff_subset, ofBoolRing_sub, bihimp_left_involutive, AlgebraicGeometry.Scheme.support_nilradical, le_sdiff_right, BiheytingHom.map_sdiff', Set.pairwise_disjoint_Ico_zsmul, WithBot.orderIsoPUnitSumLex_symm_inl, disjoint_sdiff_self_right, bihimp_bihimp_cancel_right, bihimp_eq_left, symmDiff_eq', Set.pairwise_disjoint_Ioo_mul_zpow, sup_inf_inf_compl, BooleanSubalgebra.map_map, sdiff_le_iff', inf_symmDiff_distrib_right, Set.sdiff_singleton_wcovBy, Set.image_symmDiff, bot_sdiff, sdiff_symmDiff, codisjoint_bihimp_sup, Pi.symmDiff_apply, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, toBoolRing_inf, compl_inf, sup_sdiff_right_self, symmDiff_compl_self, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, Set.disjoint_of_subset_iff_left_eq_empty, inf_himp_bihimp, SetRel.core_mono, sdiff_sdiff_sup_sdiff', BoolAlg.ext_iff, Coheyting.boundary_top, symmDiff_symmDiff_self', Finset.compl_inf, hnot_le_iff_codisjoint_left, Set.toFinset_symmDiff, WithBot.orderIsoPUnitSumLex_symm_inr, Order.Ideal.IsProper.notMem_or_compl_notMem, Coheyting.boundary_le_hnot, symmDiff_top, sup_inf_inf_sdiff, Set.isCompl_range_some_none, isLeast_sdiff, Coheyting.hnot_boundary, hnot_symmDiff_self, Set.indicator_symmDiff, symmDiff_right_comm, pairwise_disjoint_fiber, Finset.compl_sup, bihimp_right_surjective, Coheyting.hnot_eq_top_iff_exists_boundary, hnot_hnot_le, ofBoolAlg_inf, Set.symmDiff_def, Set.covBy_iff_exists_sdiff_singleton, instWellFoundedLTSubtypeSetFinite, disjoint_compl_right_iff, symmDiff_top', SetRel.prod_comp_prod, codisjoint_iff_compl_le_left, Set.disjoint_image_left, Booleanisation.comp_lt_comp, Set.sdiff_singleton_covBy, BooleanSubalgebra.inf_mem, bihimp_himp_left, symmDiff_left_inj, Types.monoOverEquivalenceSet_inverse_map, disjoint_symmDiff_inf, BoolAlg.hasForgetToBoolRing_forget₂_map, top_symmDiff, symmDiff_assoc, codisjoint_hnot_right, Finpartition.mem_avoid, sdiff_sup, Fin.top_eq_last, BiheytingHom.toFun_eq_coe_aux, Set.pairwise_disjoint_Ioc_zsmul, isCoatom_compl, sdiff_symmDiff', bihimp_eq_right, Set.subset_compl_iff_disjoint_right, BooleanSubalgebra.subtype_comp_inclusion, boolRingCatEquivBoolAlg_functor, le_hnot_inf_hnot, sdiff_inf_self_left, sdiff_le_hnot, Set.mem_symmDiff, BooleanSubalgebra.sup_mem, BoolAlg.ofHom_comp, compl_symmDiff, BooleanSubalgebra.mem_comap, SetRel.image_core_gc, Set.disjoint_sdiff_inter, ofBoolRing_add, Fin.rev_top, CoheytingHom.toFun_eq_coe_aux, Set.pairwise_disjoint_Ioo_add_intCast, Fintype.sup_disjointed, liminf_eq_top, Set.covBy_insert, disjoint_sdiff_comm, symmDiff_fst, compl_lt_self, BooleanSubalgebra.bot_mem', HasSubset.Subset.disjoint_compl_right, sdiff_le_iff_left, Fin.top_eq_zero, disjoint_of_sSup_disjoint, bot_symmDiff, himp_bihimp_left, sdiff_self, sdiff_lt_left, bihimp_left_comm, symmDiff_comm, UV.sup_sdiff_mem_of_mem_compression_of_notMem, BooleanSubalgebra.coe_map, Finset.inf_himp_right, SimpleGraph.edgeSet_eq_iff, symmDiff_sdiff_right, Set.pairwise_disjoint_Ioc_add_zsmul, BoolAlg.hom_id, WithTop.orderIsoSumLexPUnit_toLex, Set.disjoint_powerset_insert, symmDiff_left_involutive, Set.disjoint_toFinset, bihimp_left_surjective, bihimp_le_iff_left, symmDiff_sdiff_left, symmDiff_symmDiff_right, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, BoolAlg.hasForgetToHeytAlg_forget₂_map, WithTop.orderIsoSumLexPUnit_symm_inl, Coheyting.hnot_hnot_sup_boundary, Set.offDiag_mono, bihimp_le_iff_right, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, BooleanSubalgebra.mk_inf_mk, SimpleGraph.disjoint_edgeSet, iSup_eq_top, bihimp_bihimp_self, UV.le_of_mem_compression_of_notMem, CoheytingHomClass.map_top, symmDiff_right_inj, FinBoolAlg.forgetToFinPartOrdFaithful, sup_eq_sdiff_sup_sdiff_sup_inf, compl_image_latticeClosure, toBoolAlg_add, Coheyting.boundary_sup_le, Set.union_symmDiff_subset, CoheytingHomClass.toLatticeHomClass, sup_hnot_self, disjointed_add_one, BooleanSubalgebra.subtype_injective, ofBoolAlg_sup, Set.pairwise_disjoint_Ico_add_intCast, symmDiff_snd, BooleanSubalgebra.apply_coe_mem_map, Set.subset_diff, disjointed_le_id, Booleanisation.lift_le_lift, Int.isCompl_even_odd, hnot_top, himp_le, le_sup_sdiff, partialSups_disjointed, sdiff_sdiff_right, compl_lt_compl_iff_lt, sdiff_sdiff_sdiff_le_sdiff, Order.Ideal.isPrime_iff_mem_or_compl_mem, sdiff_inf_right_comm, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, toBoolAlg_add_add_mul, Set.Finite.toFinset_symmDiff, disjoint_disjointed_of_lt, Finset.diffs_compls_eq_infs, BiheytingHomClass.toLatticeHomClass, Set.nsmul_right_monotone, inf_sdiff_sup_left, compl_image_latticeClosure_eq_of_compl_image_eq_self, CoheytingHom.map_top', sup_sdiff_right, symmDiff_eq_right, symmDiff_eq, symmDiff_eq_sup_sdiff_inf, Set.mulIndicator_symmDiff, hnot_bot, WithTop.orderIsoSumLexPUnit_top, OrderIso.compl_symm_apply, le_sdiff, ofBoolRing_le_ofBoolRing_iff, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, BooleanSubalgebra.mk_sup_mk, himp_le_left, Set.disjoint_prod, Finset.inf_sdiff_right, Coheyting.boundary_inf, bihimp_eq, BooleanSubalgebra.coe_inclusion, BooleanSubalgebra.comap_id, gc_sdiff_sup, Set.indicator_eq_zero', bihimp_right_inj, bihimp_right_comm, Set.disjoint_image_iff, Set.disjoint_pi, Set.indicator_eq_zero, symmDiff_sup_inf, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, symmDiff_self, le_symmDiff_iff_right, Set.empty_covBy_singleton, symmDiff_triangle, sdiff_sdiff_self, disjoint_of_sSup_disjoint_of_le_of_le, bihimp_iff_iff, BooleanSubalgebra.latticeClosure_subset_closure, sdiff_le_inf_hnot, BooleanAlgebra.le_iff_atom_le_imp, ofBoolAlg_symmDiff, symmDiff_left_surjective, BiheytingHom.toFun_eq_coe, Set.pow_right_monotone, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, Set.apply_indicator_symmDiff, BooleanSubalgebra.infClosed, Coheyting.inf_hnot_self, sdiff_sdiff_sup_sdiff, BooleanSubalgebra.closure_latticeClosure, RingHom.asBoolAlg_id, inf_symmDiff_distrib_left, compl_le_self, Set.disjoint_compl_right_iff_subset, BoolAlg.hom_comp, Set.pairwise_disjoint_Ioo_zpow, symmDiff_isAssociative, Set.Finite.inf_of_left, gc_Ici_sInf, Set.disjoint_image_image, Set.symmDiff_subset_union, BooleanSubalgebra.mem_map_of_mem, Booleanisation.lift_sdiff_comp, eq_compl_iff_isCompl, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, BooleanSubalgebra.val_inf, Finset.sup_sdiff_right, RingHom.asBoolAlg_comp, hnot_inf_distrib, CoheytingHom.map_sdiff', Coheyting.boundary_inf_le, codisjoint_hnot_left, sdiff_eq_bot_iff, sdiff_le, BooleanSubalgebra.subtype_apply, Set.zero_mem_neg_add_iff, sdiff_sup_self, Set.pairwise_disjoint_Ioc_intCast, BooleanSubalgebra.inclusion_injective, Set.subset_compl_iff_disjoint_left, Types.monoOverEquivalenceSet_functor_map, symmDiff_isCommutative, BoolAlg.ofHom_id, sdiff_sdiff, BoolAlg.dual_map, disjoint_compl_left_iff, sdiff_inf_self_right, Set.pairwise_disjoint_Ioo_zsmul, CategoryTheory.Limits.Types.isPushout_of_bicartSq, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, Coheyting.boundary_hnot_le, boolRingCatEquivBoolAlg_inverse, compl_symmDiff_compl, Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left, SimpleGraph.fromEdgeSet_disjoint, Finset.compls_sups, BoolAlg.coe_comp, SetRel.image_mono, disjointed_le, Function.Injective.image_strictMono, BoundedLatticeHom.asBoolRing_apply, inf_sdiff_assoc, Set.disjoint_image_right, Types.monoOverEquivalenceSet_functor_obj, BooleanSubalgebra.val_sup, BoolRing.hasForgetToBoolAlg_forget₂_map, himp_bihimp_right, Function.mulSupport_disjoint_iff, Booleanisation.liftLatticeHom_injective, BoolAlg.hom_inv_apply, MeasureTheory.preVariation.sum_le, Set.pairwise_disjoint_Ioc_add_intCast, sdiff_sdiff_le, bihimp_right_involutive, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, Set.Finite.symmDiff_congr, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion', Set.inter_symmDiff_distrib_right, Booleanisation.lift_lt_lift, sdiff_inf, bihimp_eq_inf, SetRel.preimage_mono, BooleanSubalgebra.mem_map, Finset.compls_infs, Finset.coe_symmDiff, le_symmDiff_sup_left, Set.mulIndicator_eq_one', Function.support_disjoint_iff, Set.isCompl_range_inl_range_inr, Coheyting.boundary_le, sup_sdiff_left_self, sup_sdiff_self_left, Set.one_notMem_inv_mul_iff, Fin.cast_top, symmDiff_sdiff, Set.preimage_eq_empty_iff, symmDiff_sdiff_eq_sup, symmDiff_le_sup, BoolAlg.comp_apply, PUnit.top_eq, isLeast_hnot, TopologicalSpace.Clopens.surjective_finset_sup_prod, WithBot.orderIsoPUnitSumLex_toLex, ofBoolRing_mul, sdiff_sdiff_right', symmDiff_symmDiff_left, symmDiff_symmDiff_cancel_left, Set.disjoint_image_inl_image_inr, symmDiff_eq_bot, compl_antitone, Set.disjoint_sdiff_left, compl_strictAnti, gc_sSup_Iic, sdiff_compl, Set.pairwise_disjoint_Ico_zpow, inf_sdiff_sup_right, BoundedLatticeHom.asBoolRing_id, Booleanisation.comp_sup_comp, BiheytingHom.map_himp', Booleanisation.comp_sdiff_lift, Set.disjoint_preimage_iff, finBoolAlg_dual_comp_forget_to_finBddDistLat, Set.apply_mulIndicator_symmDiff, Finset.infs_compls_eq_diffs, TopologicalSpace.Clopens.coe_finset_sup, Finset.sup_sdiff_left, le_symmDiff_iff_left, SimpleGraph.IsCompleteBetween.disjoint, Set.disjoint_sdiff_right, symmDiff_le_iff, codisjoint_hnot_hnot_left_iff, UV.disjoint_of_mem_compression_of_notMem, inf_sup_symmDiff, symmDiff_eq_Xor', Booleanisation.lift_lt_comp, sdiff_le_comm, symmDiff_right_surjective, Set.zero_notMem_sub_iff, MeasureTheory.preVariation.exists_Finpartition_sum_ge, Set.one_notMem_div_iff, bihimp_left_inj, bihimp_left_injective, BoundedLatticeHom.asBoolRing_comp, MeasureTheory.preVariation.exists_Finpartition_sum_gt, Fintype.exists_disjointed_le, sdiff_sdiff_left, OrderIso.asBoolAlgAsBoolRing_apply, disjointed_succ, sSup_eq_top, Set.Finite.disjoint_toFinset, Finset.compls_infs_eq_diffs, bihimp_bihimp_cancel_left, inf_sdiff, sdiff_inf_distrib, Set.pairwiseDisjoint_range_singleton, le_symmDiff_sup_right, symmDiff_symmDiff_right', Fin.rev_zero_eq_top, Set.Finite.symmDiff, Set.disjoint_diagonal_offDiag, SetRel.gc_leftDual_rightDual, sdiff_eq_self_iff_disjoint, BooleanSubalgebra.mem_carrier, disjointed_apply, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, Booleanisation.comp_inf_comp, compl_le_compl_iff_le, Set.symmDiff_eq_empty, OrderIso.compl_apply, sup_sdiff, CoheytingHom.toFun_eq_coe, symmDiff_hnot_self, inf_sdiff_distrib_right, Set.mulIndicator_eq_one, compl_le_hnot, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, symmDiff_left_injective, sdiff_top, BooleanSubalgebra.coe_subtype, CoheytingHomClass.toBoundedLatticeHomClass, symmDiff_eq_left, Types.monoOverEquivalenceSet_inverse_obj, sdiff_bot, Booleanisation.lift_inf_lift, BooleanSubalgebra.inclusion_rfl, hnot_sup_self, symmDiff_right_injective, sdiff_eq_sdiff_iff_inf_eq_inf, maximal_subtype, Finset.sup_himp_right, compl_eq_iff_isCompl, symmDiff_eq_top, Set.one_mem_div_iff, symmDiff_sdiff_inf, Fin.range_natAdd_eq_Ioi, symmDiff_symmDiff_inf, Set.pairwise_disjoint_Ico_intCast, disjoint_disjointed, SimpleGraph.disjoint_fromEdgeSet, sdiff_symmDiff_eq_sup, sup_sdiff_distrib, sdiff_eq_left, inf_sdiff_left_comm, PUnit.sup_eq, symmDiff_eq_sup, Set.pairwiseDisjoint_fiber, Booleanisation.lift_sup_lift, WithTop.orderIsoSumLexPUnit_symm_inr, sdiff_sdiff_right_self, instWellFoundedGTUnit, bihimp_bihimp_bihimp_comm, sdiff_le_iff, le_sup_sdiff_sup_sdiff, Set.zero_notMem_neg_add_iff, Set.disjoint_image_inl_range_inr, BooleanSubalgebra.coe_comap, subsingleton_setOf_mem_iff_pairwise_disjoint, Set.pairwiseDisjoint_image_right_iff, Finset.compl_truncatedInf, BoolAlg.inv_hom_apply, Types.monoOverEquivalenceSet_unitIso, boolAlg_dual_comp_forget_to_bddDistLat, codisjoint_himp_self_left, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, BooleanSubalgebra.mem_map_equiv, sdiff_symmDiff_left, sup_sdiff_self_right, FinBoolAlg.forgetToBoolAlg_full, Finset.inf_sdiff_left, Set.symmDiff_nonempty, compl_le_iff_compl_le, Set.preimage_symmDiff, symmDiff_left_comm, BooleanSubalgebra.inclusion_apply, Set.functorToTypes_map, Set.Finite.sup, ofDual_bihimp, Nat.isCompl_even_odd, Set.subset_image_symmDiff, Set.zero_mem_sub_iff, BooleanSubalgebra.map_id, toDual_symmDiff, compl_bihimp_compl, Set.pairwiseDisjoint_image_left_iff, Set.monotone_image, Set.wcovBy_insert, hnot_anti, inf_sdiff_right, symmDiff_right_involutive, Booleanisation.lift_le_comp, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, map_symmDiff, symmDiff_symmDiff_symmDiff_comm, Fin.val_top, minimal_subtype, bihimp_eq', Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, sdiff_eq_self_iff_disjoint', hnot_le_comm, PUnit.inf_eq, sup_sdiff_self, Coheyting.boundary_sup_sup_boundary_inf, Set.covBy_iff_exists_insert, Set.disjoint_range_inl_image_inr, partialSups_add_one_eq_sup_disjointed, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, Set.pairwise_disjoint_Ico_add_zsmul, sup_sdiff_left, bihimp_isAssociative, Finpartition.parts_extendOfLE_of_eq, top_symmDiff', inf_symmDiff_symmDiff, top_sdiff', BooleanSubalgebra.supClosed, inf_sdiff_distrib_left, compl_bihimp, MeasureTheory.preVariation.sum_le_preVariationFun_of_subset, codisjoint_himp_self_right, hnot_hnot_sup_distrib, disjoint_sdiff_self_left, Types.monoOverEquivalenceSet_counitIso, Order.Ideal.IsPrime.isMaximal, sdiff_sdiff_left', FinBoolAlg.dual_map, symmDiff_symmDiff_cancel_right, OrderIso.asBoolAlgAsBoolRing_symm_apply, Finset.sup_himp_left, iSup₂_eq_top, symmDiff_bot, BoolAlg.id_apply, sup_sdiff_injOn, Fin.zero_eq_top, Pi.mulSupport_mulSingle_disjoint, disjointed_partialSups, Set.prod_subset_compl_diagonal_iff_disjoint, hnot_le_iff_codisjoint_right, BooleanAlgebra.eq_iff_atom_le_iff, Fin.rev_bot, inf_sdiff_left, toBoolRing_symmDiff, bihimp_himp_right, Booleanisation.comp_le_comp, bihimp_assoc, Finset.disjiUnion_Iic_disjointed, le_sdiff_sup, Set.symmDiff_union_subset, Coheyting.boundary_bot, Set.pairwise_disjoint_Ioo_intCast, FinBoolAlg.forgetToBoolAlgFaithful, Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right, sdiff_symmDiff_right, isAtom_compl, toBoolAlg_mul, Finset.compl_truncatedSup, sdiff_le_iff, Order.Ideal.IsPrime.mem_or_compl_mem, Function.disjoint_support_iff, bihimp_eq_bot, Set.union_symmDiff_union_subset, sup_sdiff_symmDiff, codisjoint_hnot_hnot_right_iff, Set.one_mem_inv_mul_iff, BooleanSubalgebra.comap_comap, Finpartition.avoid_parts_val, WithBot.orderIsoPUnitSumLex_bot, Fin.succ_top, BoolAlg.ofHom_apply, BoolAlg.forget_map, CoheytingAlgebra.top_sdiff, Set.disjoint_univ_pi, RingHom.asBoolAlg_toFun, bihimp_right_injective, Set.pairwiseDisjoint_singleton_iff_injOn, sdiff_triangle
toOrderBot 📖	CompOp	9 math math: bot_sdiff, bot_symmDiff, sdiff_self, symmDiff_self, sdiff_sdiff_self, sdiff_eq_bot_iff, symmDiff_eq_bot, sdiff_bot, symmDiff_bot
toSDiff 📖	CompOp	115 math math: sdiff_eq_sdiff_iff, Pi.symmDiff_def, sdiff_sup_cancel, symmDiff_le, sdiff_le_iff', bot_sdiff, Pi.symmDiff_apply, sdiff_sdiff_comm, sup_sdiff_right_self, Disjoint.sdiff_eq_right, Disjoint.disjoint_sdiff_left, isLeast_sdiff, Disjoint.sup_sdiff_cancel_left, hnot_symmDiff_self, IsCompl.symmDiff_eq_top, symmDiff_top', symmDiff_of_ge, sdiff_le_sdiff, sdiff_inf_self_left, sdiff_le_hnot, toDual_sdiff, ofDual_himp, symmDiff_fst, sdiff_le_iff_left, bot_symmDiff, sdiff_self, symmDiff_comm, sup_sdiff_cancel_right, iSup_sdiff_eq, CoheytingHomClass.map_sdiff, symmDiff_snd, Disjoint.symmDiff_eq_sup, sdiff_le_sdiff_of_sup_le_sup_right, le_sup_sdiff, sdiff_sdiff_sdiff_le_sdiff, hnot_sdiff_comm, sdiff_le_sdiff_right, inf_sdiff_sup_left, sup_sdiff_right, symmDiff_eq_sup_sdiff_inf, gc_sdiff_sup, symmDiff_sup_inf, symmDiff_self, symmDiff_triangle, sdiff_sdiff_self, sdiff_le_inf_hnot, CoheytingHom.map_sdiff', sdiff_eq_bot_iff, sdiff_le, sdiff_eq_sInf, sdiff_sup_sdiff_cancel', sdiff_sup_self, Disjoint.sdiff_eq_left, le_sdiff_iff, symmDiff_isCommutative, sdiff_sdiff, sdiff_inf_self_right, Disjoint.disjoint_sdiff_right, sdiff_sdiff_le, hnot_hnot_sdiff_distrib, sdiff_inf, le_symmDiff_sup_left, sup_sdiff_left_self, sup_sdiff_self_left, symmDiff_sdiff, symmDiff_sdiff_eq_sup, symmDiff_le_sup, symmDiff_eq_bot, inf_sdiff_sup_right, symmDiff_le_iff, inf_sup_symmDiff, sdiff_le_comm, sdiff_sdiff_left, sdiff_sup_sdiff_cancel, sdiff_inf_distrib, le_symmDiff_sup_right, hnot_sdiff, sup_sdiff, symmDiff_hnot_self, toDual_bihimp, sdiff_top, sdiff_idem, ofDual_symmDiff, sdiff_bot, symmDiff_sdiff_inf, sup_sdiff_cancel', symmDiff_symmDiff_inf, symmDiff_of_le, sdiff_symmDiff_eq_sup, sup_sdiff_distrib, sdiff_le_iff, le_sup_sdiff_sup_sdiff, sup_sdiff_self_right, sdiff_le_sdiff_left, sup_sdiff_eq_sup, ofDual_bihimp, toDual_symmDiff, inf_sdiff_right, map_symmDiff, Disjoint.le_sdiff_of_le_left, sup_sdiff_self, sup_sdiff_left, top_symmDiff', inf_symmDiff_symmDiff, sdiff_right_comm, top_sdiff', sdiff_le_sdiff_of_sup_le_sup_left, symmDiff_bot, inf_sdiff_left, sdiff_iSup_eq, le_sdiff_sup, sdiff_le_iff, Disjoint.sup_sdiff_cancel_right, CoheytingAlgebra.top_sdiff, sdiff_triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sdiff_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup toLattice toSDiff SemilatticeSup.toMax	—	—

GeneralizedHeytingAlgebra

Definitions

Name	Category	Theorems
toDistribLattice 📖	CompOp	2 math math: HeytAlg.hasForgetToLat_forget₂_map, HeytAlg.hasForgetToLat_forget₂_obj_str
toHImp 📖	CompOp	103 math math: HeytingHomClass.map_himp, himp_inf_distrib, sup_himp_self_right, Nucleus.himp_apply, Nucleus.map_himp_apply, sup_compl_le_himp, himp_triangle, IsCompl.bihimp_eq_bot, bihimp_bihimp_sup, himp_inf_le, himp_bot, Codisjoint.himp_eq_left, le_himp_comm, Nucleus.map_himp_le, le_himp_himp, himp_top, bihimp_himp_eq_inf, Heyting.Regular.coe_himp, top_bihimp, toDual_sdiff, himp_iff_imp, ofDual_himp, himp_compl, le_himp_iff_left, Pi.bihimp_apply, Pi.bihimp_def, Codisjoint.himp_le_of_right_le, himp_le_himp_right, isGreatest_himp, himp_himp, himp_eq_top_iff, himp_inf_himp_cancel, himp_inf_himp_inf_le, compl_sup_le_himp, Codisjoint.himp_eq_right, le_himp_iff', bihimp_triangle, himp_eq_himp_iff, Sublocale.himp_mem', inf_himp, bihimp_eq_sup_himp_inf, bihimp_of_le, HeytingHom.map_himp', inf_le_bihimp, bihimp_comm, Sublocale.coe_himp, le_himp_iff, le_himp_iff, Sublocale.himp_mem, compl_compl_himp_distrib, compl_le_himp, bihimp_of_ge, himp_le_himp_himp_himp, bihimp_inf_sup, Codisjoint.himp_inf_cancel_right, bihimp_self, compl_bihimp_self, gc_inf_himp, bot_himp, himp_compl_comm, sup_bihimp_bihimp, BiheytingHom.map_himp', himp_inf_self, himp_iInf_eq, himp_le_iff, iSup_himp_eq, PUnit.himp_eq, himp_left_comm, himp_le_himp_left, sup_himp_self_left, himp_bihimp_eq_inf, Codisjoint.himp_inf_cancel_left, toDual_bihimp, sup_inf_bihimp, ofDual_symmDiff, himp_self, map_bihimp, SimpleGraph.Finsubgraph.coe_himp, bot_bihimp, himp_bihimp, HeytingAlgebra.himp_bot, sup_himp_bihimp, top_himp, le_himp, ofDual_bihimp, toDual_symmDiff, bihimp_fst, bihimp_isCommutative, sup_himp_distrib, himp_le_himp, bihimp_hnot_self, bihimp_top, bihimp_snd, inf_himp_le, Codisjoint.bihimp_eq_inf, le_bihimp_iff, bihimp_eq_top, bihimp_bot, le_bihimp, Heyting.IsRegular.himp, BiheytingHomClass.map_himp, himp_idem, himp_eq_sSup
toLattice 📖	CompOp	139 math math: Heyting.isRegular_top, himp_inf_distrib, sup_himp_self_right, lt_compl_self, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Hom.preimage_bot, sup_compl_le_himp, himp_triangle, bihimp_bihimp_sup, PUnit.bot_eq, himp_inf_le, himp_bot, le_himp_comm, HeytAlg.Iso.mk_inv, le_himp_himp, Heyting.IsRegular.disjoint_compl_right_iff, himp_top, bihimp_himp_eq_inf, top_bihimp, compl_sup_compl_le, Fin.rev_top, compl_anti, Heyting.Regular.coe_sdiff, le_himp_iff_left, disjoint_compl_compl_left_iff, Pi.bihimp_apply, Pi.bihimp_def, compl_inf_eq_bot, limsup_eq_bot, BoolAlg.hasForgetToHeytAlg_forget₂_map, Heyting.Regular.coe_le_coe, PrimeSpectrum.basicOpen_zero, disjoint_compl_left, isGreatest_himp, himp_himp, disjoint_compl_compl_right_iff, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, himp_eq_top_iff, Heyting.Regular.coe_inf, himp_inf_himp_inf_le, compl_sup_le_himp, MeasureTheory.Content.innerContent_bot, le_compl_self, Heyting.Regular.coe_bot, le_himp_iff', bihimp_triangle, le_compl_iff_le_compl, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, inf_himp, Fin.bot_eq_zero, bihimp_eq_sup_himp_inf, HeytingHom.map_himp', inf_compl_self, Heyting.Regular.coe_top, inf_le_bihimp, bihimp_comm, le_himp_iff, le_himp_iff, HeytingHom.toFun_eq_coe_aux, compl_le_himp, Heyting.Regular.coe_toRegular, himp_le_himp_himp_himp, compl_compl_inf_distrib, compl_sup_distrib, TopologicalSpace.Opens.eq_bot_or_top, HeytingHomClass.toBoundedLatticeHomClass, bihimp_inf_sup, isGreatest_compl, HeytingHomClass.map_bot, bihimp_self, HeytingHomClass.toLatticeHomClass, compl_bihimp_self, gc_inf_himp, bot_himp, ProjectiveSpectrum.basicOpen_zero, compl_sup, sup_bihimp_bihimp, compl_inf_self, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, himp_inf_self, le_compl_iff_disjoint_left, Heyting.Regular.coe_lt_coe, sup_himp_self_left, himp_bihimp_eq_inf, disjoint_compl_right, le_compl_comm, Fin.rev_last_eq_bot, AlgebraicGeometry.Proj.basicOpen_zero, toDual_bihimp, Heyting.Regular.toRegular_coe, sup_inf_bihimp, ofDual_symmDiff, le_compl_compl, himp_self, map_bihimp, HeytingHom.map_bot', le_compl_iff_disjoint_right, compl_top, bot_bihimp, himp_bihimp, Heyting.Regular.coe_sup, HeytingAlgebra.himp_bot, HeytingHom.toFun_eq_coe, AlgebraicGeometry.Scheme.basicOpen_zero, iInf_eq_bot, sup_himp_bihimp, AlgebraicGeometry.isAffineOpen_bot, HeytAlg.Iso.mk_hom, iInf₂_eq_bot, top_himp, le_himp, Heyting.isRegular_bot, AlgebraicGeometry.basicOpen_eq_bot_iff, bihimp_fst, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, bihimp_isCommutative, Heyting.IsRegular.disjoint_compl_left_iff, BiheytingAlgebra.top_sdiff, sup_himp_distrib, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, bihimp_hnot_self, bihimp_top, TopologicalSpace.Opens.not_nonempty_iff_eq_bot, bihimp_snd, Heyting.IsRegular.inf, inf_himp_le, BiheytingAlgebra.sdiff_le_iff, Fin.rev_bot, le_bihimp_iff, bihimp_eq_top, bihimp_bot, sInf_eq_bot, inf_compl_eq_bot, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, compl_bot, PrimeSpectrum.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact
toOrderTop 📖	CompOp	9 math math: himp_top, top_bihimp, himp_eq_top_iff, bihimp_self, himp_self, top_himp, BiheytingAlgebra.top_sdiff, bihimp_top, bihimp_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_himp_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup toLattice HImp.himp toHImp SemilatticeInf.toMin Lattice.inf Lattice.inf_le_left Lattice.inf_le_right Lattice.le_inf	—	—

HeytingAlgebra

Definitions

Name	Category	Theorems
ofCompl 📖	CompOp	—
ofHImp 📖	CompOp	—
toBoundedOrder 📖	CompOp	8 math math: Heyting.isRegular_top, HeytAlg.hasForgetToLat_forget₂_map, Heyting.Regular.coe_top, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, HeytingHomClass.toBoundedLatticeHomClass, bot_himp, compl_top, compl_bot
toCompl 📖	CompOp	61 math math: Heyting.isRegular_top, lt_compl_self, sup_compl_le_himp, himp_bot, ofDual_hnot, compl_le_compl, compl_compl_compl, compl_sup_compl_le, compl_anti, Heyting.Regular.coe_sdiff, himp_compl, disjoint_compl_compl_left_iff, compl_inf_eq_bot, compl_eq_sSup_disjoint, disjoint_compl_left, disjoint_compl_compl_right_iff, toDual_compl, compl_sup_le_himp, le_compl_self, ofDual_compl, Disjoint.le_compl_right, le_compl_iff_le_compl, toDual_hnot, IsCompl.compl_eq, inf_compl_self, Heyting.Regular.prop, Heyting.isRegular_compl, map_compl, compl_compl_himp_distrib, compl_le_himp, Heyting.Regular.coe_toRegular, compl_compl_inf_distrib, compl_sup_distrib, isGreatest_compl, compl_bihimp_self, himp_compl_comm, compl_sup, compl_inf_self, le_compl_iff_disjoint_left, Disjoint.le_compl_left, LE.le.disjoint_compl_right, disjoint_compl_right, le_compl_comm, compl_le_hnot, le_compl_compl, le_compl_iff_disjoint_right, compl_top, bot_bihimp, Heyting.Regular.coe_sup, himp_bot, Heyting.isRegular_bot, PUnit.compl_eq, bihimp_hnot_self, SimpleGraph.Finsubgraph.coe_compl, IsCompl.eq_compl, bihimp_bot, inf_compl_eq_bot, compl_unique, compl_bot, LE.le.disjoint_compl_left, Heyting.Regular.coe_compl
toGeneralizedHeytingAlgebra 📖	CompOp	113 math math: HeytingHomClass.map_himp, Heyting.isRegular_top, Nucleus.himp_apply, lt_compl_self, HeytAlg.hasForgetToLat_forget₂_map, Nucleus.map_himp_apply, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Hom.preimage_bot, sup_compl_le_himp, PUnit.bot_eq, himp_bot, Nucleus.map_himp_le, HeytAlg.Iso.mk_inv, Heyting.IsRegular.disjoint_compl_right_iff, HeytAlg.hasForgetToLat_forget₂_obj_str, Heyting.Regular.coe_himp, compl_sup_compl_le, Fin.rev_top, compl_anti, Heyting.Regular.coe_sdiff, himp_iff_imp, himp_compl, disjoint_compl_compl_left_iff, compl_inf_eq_bot, limsup_eq_bot, BoolAlg.hasForgetToHeytAlg_forget₂_map, Heyting.Regular.coe_le_coe, PrimeSpectrum.basicOpen_zero, disjoint_compl_left, disjoint_compl_compl_right_iff, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, Heyting.Regular.coe_inf, compl_sup_le_himp, MeasureTheory.Content.innerContent_bot, le_compl_self, Heyting.Regular.coe_bot, le_compl_iff_le_compl, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, Sublocale.himp_mem', AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, Fin.bot_eq_zero, HeytingHom.map_himp', inf_compl_self, Heyting.Regular.coe_top, Sublocale.coe_himp, Sublocale.himp_mem, HeytingHom.toFun_eq_coe_aux, compl_compl_himp_distrib, compl_le_himp, Heyting.Regular.coe_toRegular, compl_compl_inf_distrib, compl_sup_distrib, TopologicalSpace.Opens.eq_bot_or_top, HeytingHomClass.toBoundedLatticeHomClass, isGreatest_compl, HeytingHomClass.map_bot, HeytingHomClass.toLatticeHomClass, compl_bihimp_self, bot_himp, himp_compl_comm, ProjectiveSpectrum.basicOpen_zero, compl_sup, compl_inf_self, BiheytingHom.map_himp', TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, le_compl_iff_disjoint_left, himp_iInf_eq, Heyting.Regular.coe_lt_coe, himp_le_iff, iSup_himp_eq, PUnit.himp_eq, disjoint_compl_right, le_compl_comm, Fin.rev_last_eq_bot, AlgebraicGeometry.Proj.basicOpen_zero, Heyting.Regular.toRegular_coe, le_compl_compl, map_bihimp, HeytingHom.map_bot', SimpleGraph.Finsubgraph.coe_himp, le_compl_iff_disjoint_right, compl_top, bot_bihimp, Heyting.Regular.coe_sup, himp_bot, HeytingHom.toFun_eq_coe, AlgebraicGeometry.Scheme.basicOpen_zero, iInf_eq_bot, AlgebraicGeometry.isAffineOpen_bot, HeytAlg.Iso.mk_hom, iInf₂_eq_bot, Heyting.isRegular_bot, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, Heyting.IsRegular.disjoint_compl_left_iff, BiheytingAlgebra.top_sdiff, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, bihimp_hnot_self, TopologicalSpace.Opens.not_nonempty_iff_eq_bot, Heyting.IsRegular.inf, BiheytingAlgebra.sdiff_le_iff, Fin.rev_bot, bihimp_bot, sInf_eq_bot, inf_compl_eq_bot, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, compl_bot, Heyting.IsRegular.himp, PrimeSpectrum.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, BiheytingHomClass.map_himp, himp_eq_sSup
toOrderBot 📖	CompOp	551 math math: IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Set.Finite.t2_separation, Set.pairwiseDisjoint_range_iff, Matroid.exists_isBasis_disjoint_isBasis_of_subset, Metric.ball_disjoint_ball, Set.pairwise_disjoint_Ioc_zpow, Set.pairwiseDisjoint_pair_insert, Set.pairwise_disjoint_Ioo_add_zsmul, Metric.disjoint_ball_infDist, Set.disjoint_ordT5Nhd, LocalizedModule.subsingleton_iff_disjoint, Finpartition.isPartition_parts, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, Sym2.disjoint_diagSet_fromRel, Set.disjoint_compl_left_iff_subset, SimpleGraph.isBipartiteWith_neighborSet_disjoint, SeparatedNhds.disjoint, PrimeSpectrum.localization_specComap_range, Set.pairwise_disjoint_Ico_zsmul, disjoint_or_subset_of_isClopen, BoxIntegral.Box.disjoint_splitCenterBox, lt_compl_self, Matroid.isBase_compl_iff_maximal_disjoint_isBase, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt, Set.pairwise_disjoint_Ioo_mul_zpow, Disjoint.of_span₀, MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Hom.preimage_bot, UpperSet.sdiff_eq_left, IsCompl.bihimp_eq_bot, MeasureTheory.pairwise_disjoint_fundamentalInterior, PUnit.bot_eq, SeparatedNhds.disjoint_closure_left, Set.Iio_disjoint_Ioi_of_not_lt, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, Set.disjoint_of_subset_iff_left_eq_empty, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, IsUltrametricDist.ball_subset_trichotomy, Matroid.IsBasis.contract_dep_iff, BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, SimpleGraph.ComponentCompl.disjoint_right, LowerSet.disjoint_coe, AddAction.orbit.pairwiseDisjoint, EMetric.ball_disjoint, Topology.RelCWComplex.pairwiseDisjoint', Matroid.contract_isCocircuit_iff, Finset.compl_inf, BoxIntegral.Box.disjoint_withBotCoe, Antitone.pairwise_disjoint_on_Ioc_pred, Topology.RelCWComplex.disjoint_openCell_of_ne, IsCompact.separation_of_notMem, Finset.isWF_sup, AddAction.IsBlock.disjoint_vadd_left, himp_bot, OrderedFinpartition.disjoint, sSup_disjoint_iff, Set.Iio_disjoint_Ioi_iff, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, exists_dist_slope_lt_pairwiseDisjoint_hasSum, Besicovitch.exist_disjoint_covering_families, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, MeasureTheory.exists_null_pairwise_disjoint_diff, pairwise_disjoint_fiber, Finset.compl_sup, Matroid.IsBasis.contract_indep_iff, separated_by_continuous, Antitone.pairwise_disjoint_on_Ioo_pred, Perfect.small_diam_splitting, SimpleGraph.ComponentCompl.pairwise_disjoint, Set.Iic_disjoint_Ioi, disjoint_compl_right_iff, Set.disjoint_pi_univ_Ioc_update_left_right, SetRel.prod_comp_prod, disjoint_nested_nhds_of_not_inseparable, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, Set.disjoint_image_left, exists_disjoint_vadd_of_isCompact, MulAction.IsBlock.disjoint_smul_of_ne, Heyting.IsRegular.disjoint_compl_right_iff, Disjoint.of_span, Matroid.IsMinor.exists_eq_contract_delete_disjoint, isEmbedding_sumElim, Matroid.delete_eq_self_iff, MulAction.isBlock_iff_smul_eq_or_disjoint, disjoint_interior_frontier, Matroid.contract_eq_self_iff, Finset.sup_set_eq_biUnion, AlgebraicIndependent.adjoin_iff_disjoint, MeasureTheory.IsSetSemiring.disjointOfUnion_props, Set.pairwise_disjoint_Ioc_zsmul, isCoatom_compl, Set.subset_compl_iff_disjoint_right, Set.Ioc_disjoint_Ioc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, UpperSet.codisjoint_coe, Matroid.Coindep.delete_spanning_iff, Monotone.pairwise_disjoint_on_Ioc_pred, Set.disjoint_right_ordSeparatingSet, LowerSet.sdiff_eq_left, Antitone.pairwise_disjoint_on_Ioo_succ, Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_card, Set.disjoint_sdiff_inter, Fin.rev_top, Set.pairwise_disjoint_Ioo_add_intCast, Set.pairwise_disjoint_vadd_iff, Set.disjoint_iUnion_left, HasSubset.Subset.disjoint_compl_right, disjoint_compl_compl_left_iff, Set.definable_finset_sup, disjoint_of_sSup_disjoint, MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier, Set.PairwiseDisjoint.exists_mem_filter, NonarchimedeanGroup.exists_openSubgroup_separating, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, Finset.inf_himp_right, SimpleGraph.edgeSet_eq_iff, Ideal.disjoint_powers_iff_notMem, Matroid.Indep.contract_dep_iff, Set.pairwise_disjoint_Ioc_add_zsmul, SimpleGraph.disjoint_edge, MeasureTheory.IsSetSemiring.mem_supClosure_iff, compl_inf_eq_bot, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, disjoint_nhdsSet_principal, Set.disjoint_powerset_insert, Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, MulAction.disjoint_image_image_iff, t2_separation_nhds, Set.disjoint_toFinset, limsup_eq_bot, SimpleGraph.disjoint_edgeFinset, Setoid.IsPartition.finpartition_parts, Set.disjoint_smul_set, AddAction.IsBlock.disjoint_vadd_vadd_set, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, Filter.disjoint_iff, Ideal.disjoint_map_primeCompl_iff_comap_le, AddAction.IsBlock.vadd_eq_vadd_or_disjoint, not_disjoint_segment_convexHull_triple, compl_eq_sSup_disjoint, Set.disjoint_sUnion_left, NonarchimedeanAddGroup.exists_openAddSubgroup_separating, TopologicalSpace.Clopens.coe_disjoint, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, LowerSet.sdiff_lt_left, SimpleGraph.disjoint_edgeSet, Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes, Besicovitch.exist_finset_disjoint_balls_large_measure, isInducing_sumElim, PrimeSpectrum.basicOpen_zero, disjoint_iSup_iff, Set.Ioi_disjoint_Iio_iff, Matroid.dual_indep_iff_exists', MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux, MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier, AddAction.IsBlock.pairwiseDisjoint_range_vadd, disjoint_compl_left, Set.pairwise_disjoint_Ico_add_intCast, Set.isAtom_singleton, Set.PairwiseDisjoint.exists_mem_filter_basis, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, MulAction.orbit.eq_or_disjoint, Topology.IsInducing.disjoint_of_sumElim_aux, disjoint_compl_compl_right_iff, Set.subset_diff, separated_by_isOpenEmbedding, Setoid.eqv_classes_disjoint, IsLocalization.isPrime_iff_isPrime_disjoint, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, SubMulAction.disjoint_val_image, AddAction.IsBlock.disjoint_vadd_set_vadd, Metric.disjoint_closedEBall_of_lt_infEDist, exists_nhds_disjoint_closure, TopologicalSpace.Opens.coe_finset_sup, SimpleGraph.EdgeLabeling.pairwise_disjoint_labelGraph, isNowhereDense_iff_disjoint, ConvexCone.disjoint_hull_left_of_convex, EisensteinSeries.pairwise_disjoint_gammaSet, Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card, MulAction.IsBlock.disjoint_smul_right, BoxIntegral.unitPartition.disjoint, MeasureTheory.Content.innerContent_bot, MulAction.IsBlock.disjoint_smul_smul_set, AlgebraicGeometry.disjoint_opensRange_sigmaι, Set.pairwiseDisjoint_prod_left, le_compl_self, Set.disjoint_iUnion_right, LowerSet.disjoint_prod, exists_open_nhds_disjoint_closure, disjoint_measurableAtom_of_notMem, MeasureTheory.disjoint_cylinder_iff, NFA.disjoint_evalFrom_reverse_iff, Matroid.contract_spanning_iff, Set.disjoint_prod, Heyting.Regular.coe_bot, Topology.CWComplex.pairwiseDisjoint', MulAction.IsBlock.disjoint_smul_set_smul, Set.indicator_eq_zero', Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem, disjoint_frontier_iff_isOpen, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall, MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, IsGenericPoint.disjoint_iff, Set.disjoint_image_iff, AddAction.IsBlock.disjoint_vadd_right, iSup_disjoint_iff, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, Set.disjoint_pi, MeasureTheory.IsSetSemiring.diff_eq_sUnion', Antitone.pairwise_disjoint_on_Ioc_succ, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, Set.indicator_eq_zero, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, exists_seq_infinite_isOpen_pairwise_disjoint, disjoint_of_sSup_disjoint_of_le_of_le, Set.disjoint_iUnion₂_right, IsUltrametricDist.ball_eq_or_disjoint, Filter.HasBasis.disjoint_iff, BooleanSubalgebra.mem_closure_iff_sup_sdiff, AddAction.isBlock_iff_vadd_eq_or_disjoint, Set.exists_union_disjoint_cardinal_eq_of_even, SimpleGraph.pairwise_disjoint_supp_connectedComponent, IsRetrocompact.finsetSup, Set.Ioi_disjoint_Iio_of_le, BoxIntegral.Prepartition.pairwiseDisjoint, Set.disjoint_compl_right_iff_subset, Set.pairwise_disjoint_Ioo_zpow, Metric.ball_disjoint_closedBall, Matroid.IsCircuit.disjoint_coloops, Set.disjoint_image_image, UpperSet.lt_sdiff_left, Subgroup.IsComplement.pairwiseDisjoint_smul, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, Fin.bot_eq_zero, VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype, Finset.intervalGapsWithin_pairwiseDisjoint_Ioc, inf_compl_self, SimpleGraph.EdgeLabeling.pairwiseDisjoint_univ_labelGraph, MulAction.IsBlock.smul_eq_smul_or_disjoint, ConvexCone.disjoint_coe, TopologicalSpace.Compacts.coe_finset_sup, Filter.disjoint_principal_principal, iSup₂_disjoint_iff, connectedComponent_disjoint, AddAction.IsBlock.disjoint_vadd_of_ne, Set.zero_mem_neg_add_iff, Set.pairwise_disjoint_Ioc_intCast, Set.subset_compl_iff_disjoint_left, ProperlyDiscontinuousSMul.exists_nhds_disjoint_image, Topology.RelCWComplex.disjoint_interior_base_closedCell, Set.Iic_disjoint_Ioc, Prop.isAtom_iff, SimpleGraph.IsBipartiteWith.disjoint, SeparatedNhds.disjoint_closure_right, Set.Ioc_disjoint_Ioi, disjoint_compl_left_iff, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, Set.pairwise_disjoint_Ioo_zsmul, Set.Iic_disjoint_Ici, Set.isAtom_iff, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, disjoint_ball_closedBall_iff, SimpleGraph.fromEdgeSet_disjoint, SimpleGraph.isBipartiteWith_neighborSet_disjoint', Interval.disjoint_coe, Set.disjoint_image_right, Set.Ioi_disjoint_Iio_of_not_lt, VitaliFamily.covering, Finset.isPWO_sup, Finset.partiallyWellOrderedOn_sup, Function.mulSupport_disjoint_iff, exists_open_convex_of_notMem, SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint, AddAction.isBlock_iff_disjoint_vadd_of_ne, Vitali.exists_disjoint_subfamily_covering_enlargement, Matroid.coindep_contract_iff, t2_separation_compact_nhds, MeasureTheory.preVariation.sum_le, IndexedPartition.disjoint, TopologicalSpace.Opens.eq_bot_or_top, Set.pairwise_disjoint_Ioc_add_intCast, Set.Ico_disjoint_Ico, AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, Topology.RelCWComplex.disjointBase, Monotone.pairwise_disjoint_on_Ico_pred, isGreatest_compl, Metric.disjoint_closedBall_of_lt_infDist, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, Metric.frontier_thickening_disjoint, MulAction.isBlock_iff_smul_eq_smul_or_disjoint, AddAction.isBlock_iff_pairwiseDisjoint_range_vadd, TopologicalSpace.Closeds.coe_finset_sup, HeytingHomClass.map_bot, Vitali.exists_disjoint_covering_ae, ProperlyDiscontinuousVAdd.exists_nhds_disjoint_image, Monotone.pairwise_disjoint_on_Ioo_succ, disjoint_sSup_iff, Metric.AreSeparated.disjoint, Set.Ioi_disjoint_Iio_same, Set.mulIndicator_eq_one', BoxIntegral.Box.disjoint_coe, MulAction.IsBlock.disjoint_smul_left, Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite, IsLowerSet.disjoint_upperClosure_left, Function.support_disjoint_iff, MulAction.isBlock_iff_disjoint_smul_of_ne, Besicovitch.exists_disjoint_closedBall_covering_ae, AddSubgroup.IsComplement.pairwiseDisjoint_vadd, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, IsLocalization.orderIsoOfPrime_symm_apply_coe, Matroid.dual_indep_iff_exists, FreeGroup.startsWith.disjoint_iff_ne, Set.disjoint_vadd_set, disjoint_closedBall_closedBall_iff, Set.one_notMem_inv_mul_iff, Set.disjoint_sUnion_right, T2Space.t2, compl_bihimp_self, Set.preimage_eq_empty_iff, bot_himp, AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint, Metric.closedBall_disjoint_ball, TopologicalSpace.Clopens.surjective_finset_sup_prod, IsLocalization.disjoint_comap_iff, ProjectiveSpectrum.basicOpen_zero, AddAction.orbit.eq_or_disjoint, t2Space_iff_nhds, Set.disjoint_image_inl_image_inr, IsLowerSet.disjoint_upperClosure_right, Monotone.pairwise_disjoint_on_Ioo_pred, Set.disjoint_sdiff_left, Set.ncard_union_eq_iff, Monotone.pairwise_disjoint_on_Ioc_succ, Set.pairwise_disjoint_Ico_zpow, compl_inf_self, Matroid.delete_dep_iff, Set.disjoint_preimage_iff, MeasureTheory.exists_subordinate_pairwise_disjoint, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, TopologicalSpace.Clopens.coe_finset_sup, Finset.sup_sdiff_left, disjoint_principal_nhdsSet, Matroid.contract_spanning_iff', Set.exists_union_disjoint_cardinal_eq_iff, le_compl_iff_disjoint_left, SimpleGraph.IsCompleteBetween.disjoint, Set.disjoint_sdiff_right, Matroid.Indep.contract_indep_iff, Metric.frontier_cthickening_disjoint, MulAction.orbit.pairwiseDisjoint, Set.Iio_disjoint_Ioi_same, Topology.RelCWComplex.disjoint_skeleton_openCell, RootedTree.subtrees_disjoint, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, Set.zero_notMem_sub_iff, MeasureTheory.preVariation.exists_Finpartition_sum_ge, Set.one_notMem_div_iff, Metric.eball_disjoint, MeasureTheory.preVariation.exists_Finpartition_sum_gt, MeasureTheory.AEDisjoint.exists_disjoint_diff, disjoint_ball_ball_iff, Set.Finite.disjoint_toFinset, LE.le.disjoint_compl_right, Topology.RelCWComplex.disjointBase', Set.pairwiseDisjoint_range_singleton, TopologicalSpace.Closeds.isAtom_coe, SimpleGraph.disjoint_left, disjoint_memPartition, Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, NFA.disjoint_stepSet_reverse, Set.disjoint_diagonal_offDiag, PiNat.disjoint_cylinder_of_longestPrefix_lt, IsUpperSet.disjoint_lowerClosure_left, IsUltrametricDist.closedBall_subset_trichotomy, Set.disjoint_vadd_set_left, SimpleGraph.disjoint_image_val_universalVerts, ConvexCone.disjoint_hull_right_of_convex, disjoint_compl_right, Set.Ioc_disjoint_Ioc_of_le, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, EMetric.disjoint_closedBall_of_lt_infEdist, Set.pairwiseDisjoint_vadd_iff, Set.mulIndicator_eq_one, Ideal.disjoint_primeCompl_of_liesOver, Fin.rev_last_eq_bot, AlgebraicGeometry.Proj.basicOpen_zero, Composition.disjoint_range, MulAction.IsBlock.pairwiseDisjoint_range_smul, MulAction.isBlock_iff_pairwiseDisjoint_range_smul, isSeparatedMap_iff_nhds, Set.exists_union_disjoint_ncard_eq_of_even, Set.Ici_disjoint_Iic, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem, Finset.sup_himp_right, Set.one_mem_div_iff, Matroid.delete_isBasis_iff, HeytingHom.map_bot', Set.pairwise_disjoint_Ico_intCast, le_compl_iff_disjoint_right, compl_top, Set.pairwiseDisjoint_iff, SimpleGraph.disjoint_fromEdgeSet, TopologicalSpace.Opens.coe_disjoint, bot_bihimp, Set.pairwiseDisjoint_fiber, CompleteAtomicBooleanAlgebra.instIsAtomistic, Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter, PMF.toOuterMeasure_apply_eq_zero_iff, AddAction.disjoint_image_image_iff, himp_bot, DoubleCoset.disjoint_out, AlgebraicGeometry.Scheme.basicOpen_zero, Finset.wellFoundedOn_sup, AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux, Set.disjoint_vadd_set_right, iInf_eq_bot, Set.zero_notMem_neg_add_iff, Set.disjoint_image_inl_range_inr, subsingleton_setOf_mem_iff_pairwise_disjoint, Set.pairwiseDisjoint_image_right_iff, Set.Iio_disjoint_Ici, Topology.RelCWComplex.disjoint_skeletonLT_openCell, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff, AlgebraicGeometry.isAffineOpen_bot, iInf₂_eq_bot, ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, Set.pairwise_disjoint_smul_iff, Setoid.IsPartition.pairwiseDisjoint, ModelWithCorners.disjoint_interior_boundary, sSupIndep_iff_pairwiseDisjoint, Set.Ico_disjoint_Ico_same, Finset.inf_sdiff_left, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, Heyting.isRegular_bot, SubAddAction.disjoint_val_image, BoxIntegral.Prepartition.disjoint_coe_of_mem, MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd, Antitone.pairwise_disjoint_on_Ico_pred, Matroid.Indep.contract_isBase_iff, Pairwise.exists_mem_filter_basis_of_disjoint, Set.pairwiseDisjoint_smul_iff, MulAction.IsBlock.smul_eq_or_disjoint, Set.zero_mem_sub_iff, Set.Ioo_disjoint_Ioo, Perfect.splitting, Metric.sphere_disjoint_ball, AlgebraicGeometry.basicOpen_eq_bot_iff, RealRMK.range_cut_partition, Set.pairwiseDisjoint_image_left_iff, Besicovitch.exists_disjoint_closedBall_covering_ae_aux, Ideal.exists_disjoint_powers_of_span_eq_top, MeasureTheory.pairwise_disjoint_addFundamentalInterior, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, Topology.RelCWComplex.pairwiseDisjoint, Matroid.Coindep.delete_isBase_iff, Set.disjoint_smul_set_left, disjoint_nhdsWithin_of_mem_discrete, Filter.NeBot.not_disjoint, Set.disjoint_smul_set_right, Matroid.dualIndepMatroid_Indep, PrimeSpectrum.localization_comap_range, IsLocalization.orderIsoOfPrime_apply_coe, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, MeasurableSpace.disjoint_countablePartition, Heyting.IsRegular.disjoint_compl_left_iff, Set.disjoint_range_inl_image_inr, VitaliFamily.FineSubfamilyOn.covering_disjoint, exists_disjoint_smul_of_isCompact, disjoint_nested_nhds, Matroid.IsBasis'.contract_dep_iff, Matroid.delete_indep_iff, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, MeasureTheory.IsSetRing.finsetSup_mem, Pairwise.exists_mem_filter_of_disjoint, Set.pairwise_disjoint_Ico_add_zsmul, Set.disjoint_left_ordSeparatingSet, MeasureTheory.IsSetSemiring.exists_finpartition_diff, Matroid.Indep.disjoint_loops, Set.Iio_disjoint_Ioi_of_le, bihimp_hnot_self, Finset.pairwiseDisjoint_pair_insert, Finsupp.disjoint_supported_supported_iff, Set.instIsAtomistic, MeasureTheory.preVariation.sum_le_preVariationFun_of_subset, Urysohns.CU.disjoint_C_support_lim, IsUpperSet.disjoint_lowerClosure_right, TopologicalSpace.Opens.not_nonempty_iff_eq_bot, Order.Ideal.PrimePair.disjoint, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom, Disjoint.exists_mem_filter_basis, Finset.sup_himp_left, IsLocalization.map_algebraMap_ne_top_iff_disjoint, iSupIndep_iff_pairwiseDisjoint, SimpleGraph.deleteEdges_eq_self, Matroid.delete_isCircuit_iff, Set.disjoint_iUnion₂_left, Pi.mulSupport_mulSingle_disjoint, Set.prod_subset_compl_diagonal_iff_disjoint, SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem, Fin.rev_bot, r1_separation, Finset.sup_id_set_eq_sUnion, bihimp_bot, NumberField.InfinitePlace.disjoint_isReal_isComplex, Vitali.exists_disjoint_covering_ae', AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero, Matroid.IsBasis'.contract_indep_iff, IsCoatom.of_compl, sInf_eq_bot, disjoint_iSup₂_iff, inf_compl_eq_bot, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff, disjoint_closedBall_ball_iff, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, IsCoatom.compl, Set.pairwise_disjoint_Ioo_intCast, PiNat.exists_disjoint_cylinder, t2_separation, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, compl_bot, isAtom_compl, NumberField.mixedEmbedding.disjoint_negAt_plusPart, PMF.toMeasure_apply_eq_zero_iff, Set.Ioc_disjoint_Ioi_same, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion, Topology.RelCWComplex.disjoint_base_iUnion_openCell, AddAction.IsBlock.vadd_eq_or_disjoint, IsUltrametricDist.closedBall_eq_or_disjoint, Concept.disjoint_extent_intent, Function.disjoint_support_iff, PrimeSpectrum.basicOpen_eq_bot_iff, LE.le.disjoint_compl_left, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, Set.one_mem_inv_mul_iff, Antitone.pairwise_disjoint_on_Ico_succ, Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell, Metric.closedBall_disjoint_closedBall, t2Space_iff, Set.disjoint_univ_pi, Set.pairwiseDisjoint_singleton_iff_injOn, Monotone.pairwise_disjoint_on_Ico_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
himp_bot 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp toGeneralizedHeytingAlgebra Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice toOrderBot Compl.compl toCompl	—	—

IsCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_eq 📖	mathematical	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toBoundedOrder	Compl.compl HeytingAlgebra.toCompl	—	LE.le.antisymm' Disjoint.le_compl_left disjoint Disjoint.le_of_codisjoint disjoint_compl_left codisjoint
eq_compl 📖	mathematical	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toBoundedOrder	Compl.compl HeytingAlgebra.toCompl	—	LE.le.antisymm Disjoint.le_compl_right disjoint Disjoint.le_of_codisjoint disjoint_compl_left Codisjoint.symm codisjoint
eq_hnot 📖	mathematical	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toBoundedOrder	HNot.hnot CoheytingAlgebra.toHNot	—	LE.le.antisymm' Codisjoint.hnot_le_left codisjoint Disjoint.le_of_codisjoint disjoint codisjoint_hnot_right
hnot_eq 📖	mathematical	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toBoundedOrder	HNot.hnot CoheytingAlgebra.toHNot	—	LE.le.antisymm Codisjoint.hnot_le_right codisjoint Disjoint.le_of_codisjoint Disjoint.symm disjoint codisjoint_hnot_right

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codisjoint_hnot_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra	Codisjoint CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	Codisjoint.mono_right codisjoint_hnot_left
codisjoint_hnot_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra	Codisjoint CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	Codisjoint.mono_left codisjoint_hnot_right
disjoint_compl_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra	Disjoint HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	Disjoint.mono_right disjoint_compl_left
disjoint_compl_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra	Disjoint HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	Disjoint.mono_left disjoint_compl_right

LinearOrder

Definitions

Name	Category	Theorems
toBiheytingAlgebra 📖	CompOp	—

OrderDual

Definitions

Name	Category	Theorems
instBiheytingAlgebra 📖	CompOp	—
instCoheytingAlgebra 📖	CompOp	2 math math: ofDual_hnot, toDual_compl
instGeneralizedCoheytingAlgebra 📖	CompOp	2 math math: toDual_bihimp, ofDual_symmDiff
instGeneralizedHeytingAlgebra 📖	CompOp	4 math math: toDual_sdiff, ofDual_himp, ofDual_bihimp, toDual_symmDiff
instHeytingAlgebra 📖	CompOp	2 math math: ofDual_compl, toDual_hnot

PUnit

Definitions

Name	Category	Theorems
instBiheytingAlgebra 📖	CompOp	17 math math: WithBot.orderIsoPUnitSumLex_symm_inl, bot_eq, WithBot.orderIsoPUnitSumLex_symm_inr, WithTop.orderIsoSumLexPUnit_toLex, WithTop.orderIsoSumLexPUnit_symm_inl, WithTop.orderIsoSumLexPUnit_top, hnot_eq, top_eq, WithBot.orderIsoPUnitSumLex_toLex, sdiff_eq, himp_eq, sup_eq, WithTop.orderIsoSumLexPUnit_symm_inr, instWellFoundedGTUnit, compl_eq, inf_eq, WithBot.orderIsoPUnitSumLex_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra BiheytingAlgebra.toHeytingAlgebra instBiheytingAlgebra HeytingAlgebra.toOrderBot	—	—
compl_eq 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl BiheytingAlgebra.toHeytingAlgebra instBiheytingAlgebra	—	—
himp_eq 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra BiheytingAlgebra.toHeytingAlgebra instBiheytingAlgebra	—	—
hnot_eq 📖	mathematical	—	HNot.hnot BiheytingAlgebra.toHNot instBiheytingAlgebra	—	—
inf_eq 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra instBiheytingAlgebra	—	—
sdiff_eq 📖	mathematical	—	BiheytingAlgebra.toSDiff instBiheytingAlgebra	—	—
sup_eq 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra instBiheytingAlgebra	—	—
top_eq 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra instBiheytingAlgebra CoheytingAlgebra.toOrderTop	—	—

Pi

Definitions

Name	Category	Theorems
instBiheytingAlgebra 📖	CompOp	—
instCoheytingAlgebra 📖	CompOp	—
instGeneralizedCoheytingAlgebra 📖	CompOp	—
instGeneralizedHeytingAlgebra 📖	CompOp	—
instHImpForall 📖	CompOp	4 math math: himp_apply, bihimp_apply, bihimp_def, himp_def
instHNotForall 📖	CompOp	2 math math: hnot_def, hnot_apply
instHeytingAlgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
himp_apply 📖	mathematical	—	HImp.himp instHImpForall	—	—
himp_def 📖	mathematical	—	HImp.himp instHImpForall	—	—
hnot_apply 📖	mathematical	—	HNot.hnot instHNotForall	—	—
hnot_def 📖	mathematical	—	HNot.hnot instHNotForall	—	—

Prod

Definitions

Name	Category	Theorems
instBiheytingAlgebra 📖	CompOp	—
instCoheytingAlgebra 📖	CompOp	—
instCompl 📖	CompOp	2 math math: snd_compl, fst_compl
instGeneralizedCoheytingAlgebra 📖	CompOp	—
instGeneralizedHeytingAlgebra 📖	CompOp	—
instHImp 📖	CompOp	4 math math: snd_himp, fst_himp, bihimp_fst, bihimp_snd
instHNot 📖	CompOp	2 math math: snd_hnot, fst_hnot
instHeytingAlgebra 📖	CompOp	—
instSDiff 📖	CompOp	4 math math: symmDiff_fst, symmDiff_snd, snd_sdiff, fst_sdiff

Prop

Definitions

Name	Category	Theorems
instHeytingAlgebra 📖	CompOp	2 math math: himp_iff_imp, isAtom_iff

(root)

Definitions

Name	Category	Theorems
BiheytingAlgebra 📖	CompData	—
CoheytingAlgebra 📖	CompData	—
GeneralizedCoheytingAlgebra 📖	CompData	—
GeneralizedHeytingAlgebra 📖	CompData	—
HeytingAlgebra 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_himp 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toOrderBot Top.top OrderTop.toTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderTop HeytingAlgebra.toBoundedOrder	—	himp_eq_top_iff bot_le
bot_sdiff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	—	sdiff_eq_bot_iff bot_le
codisjoint_hnot_hnot_left_iff 📖	mathematical	—	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	hnot_hnot_hnot
codisjoint_hnot_hnot_right_iff 📖	mathematical	—	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	hnot_hnot_hnot
codisjoint_hnot_left 📖	mathematical	—	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	Codisjoint.symm codisjoint_hnot_right
codisjoint_hnot_right 📖	mathematical	—	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	codisjoint_iff_le_sup sdiff_le_iff Eq.le top_sdiff'
compl_anti 📖	mathematical	—	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	le_compl_comm LE.le.trans le_compl_compl
compl_bot 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot Top.top OrderTop.toTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderTop HeytingAlgebra.toBoundedOrder	—	himp_bot himp_self
compl_compl_compl 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl	—	LE.le.antisymm compl_anti le_compl_compl
compl_compl_himp_distrib 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra	—	le_antisymm le_himp_iff compl_compl_inf_distrib compl_anti himp_inf_le le_compl_comm LE.le.trans compl_sup_le_himp compl_sup_distrib le_compl_iff_disjoint_right disjoint_right_comm inf_himp_le
compl_compl_inf_distrib 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra	—	LE.le.antisymm LE.le.trans compl_anti compl_sup_compl_le Eq.le compl_sup_distrib le_compl_iff_disjoint_right disjoint_assoc disjoint_compl_compl_left_iff disjoint_left_comm inf_comm disjoint_compl_right
compl_iff_not 📖	mathematical	—	Compl.compl Prop.instCompl	—	—
compl_inf_eq_bot 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	compl_inf_self
compl_inf_self 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	Disjoint.eq_bot disjoint_compl_left
compl_le_compl 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra	Compl.compl HeytingAlgebra.toCompl	—	compl_anti
compl_le_himp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl HImp.himp GeneralizedHeytingAlgebra.toHImp	—	LE.le.trans Eq.ge himp_bot himp_le_himp_left bot_le
compl_le_hnot 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra Compl.compl HeytingAlgebra.toCompl BiheytingAlgebra.toHeytingAlgebra HNot.hnot BiheytingAlgebra.toHNot	—	Disjoint.le_of_codisjoint disjoint_compl_left codisjoint_hnot_right
compl_ne_self 📖	—	—	—	—	ne_compl_self
compl_sup 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf	—	compl_sup_distrib
compl_sup_compl_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup Compl.compl HeytingAlgebra.toCompl SemilatticeInf.toMin	—	sup_le compl_anti inf_le_left inf_le_right
compl_sup_distrib 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf	—	sup_himp_distrib
compl_sup_le_himp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup Compl.compl HeytingAlgebra.toCompl HImp.himp GeneralizedHeytingAlgebra.toHImp	—	sup_le compl_le_himp le_himp
compl_top 📖	mathematical	—	Compl.compl HeytingAlgebra.toCompl Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra BoundedOrder.toOrderTop HeytingAlgebra.toBoundedOrder Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	eq_of_forall_le_iff le_compl_iff_disjoint_right disjoint_top le_bot_iff
compl_unique 📖	mathematical	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot SemilatticeSup.toMax Top.top OrderTop.toTop SemilatticeInf.toPartialOrder BoundedOrder.toOrderTop HeytingAlgebra.toBoundedOrder	Compl.compl HeytingAlgebra.toCompl	—	IsCompl.compl_eq IsCompl.of_eq
disjoint_compl_compl_left_iff 📖	mathematical	—	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	compl_compl_compl
disjoint_compl_compl_right_iff 📖	mathematical	—	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	compl_compl_compl
disjoint_compl_left 📖	mathematical	—	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	disjoint_iff_inf_le le_himp_iff Eq.ge himp_bot
disjoint_compl_right 📖	mathematical	—	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	Disjoint.symm disjoint_compl_left
fst_compl 📖	mathematical	—	Compl.compl Prod.instCompl	—	—
fst_himp 📖	mathematical	—	HImp.himp Prod.instHImp	—	—
fst_hnot 📖	mathematical	—	HNot.hnot Prod.instHNot	—	—
fst_sdiff 📖	mathematical	—	Prod.instSDiff	—	—
gc_inf_himp 📖	mathematical	—	GaloisConnection PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice SemilatticeInf.toMin HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff'
gc_sdiff_sup 📖	mathematical	—	GaloisConnection PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sdiff_le_iff
himp_bot 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toOrderBot Compl.compl HeytingAlgebra.toCompl	—	HeytingAlgebra.himp_bot
himp_compl 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	himp_bot himp_himp inf_idem
himp_compl_comm 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	himp_left_comm
himp_eq_himp_iff 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	inf_of_le_right
himp_eq_top_iff 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	top_le_iff le_himp_iff top_inf_eq
himp_himp 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice	—	eq_of_forall_le_iff inf_assoc
himp_idem 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	himp_himp inf_idem
himp_iff_imp 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Prop.instHeytingAlgebra	—	—
himp_inf_distrib 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice	—	eq_of_forall_le_iff
himp_inf_himp_cancel 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice	SemilatticeInf.toMin HImp.himp GeneralizedHeytingAlgebra.toHImp	—	LE.le.antisymm himp_triangle le_inf himp_le_himp_left himp_le_himp_right
himp_inf_himp_inf_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice SemilatticeInf.toMin HImp.himp GeneralizedHeytingAlgebra.toHImp	—	himp_le_himp_himp_himp
himp_inf_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice SemilatticeInf.toMin HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff le_rfl
himp_inf_self 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	inf_comm inf_himp
himp_le_himp 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	LE.le.trans himp_le_himp_right himp_le_himp_left
himp_le_himp_himp_himp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff inf_assoc himp_inf_self inf_le_left
himp_le_himp_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff LE.le.trans himp_inf_le
himp_le_himp_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff LE.le.trans inf_le_inf_left himp_inf_le
himp_left_comm 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp	—	himp_himp inf_comm
himp_ne_himp_iff 📖	—	—	—	—	Iff.not himp_eq_himp_iff
himp_self 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	—	top_le_iff le_himp_iff inf_le_right
himp_top 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	—	himp_eq_top_iff le_top
himp_triangle 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice SemilatticeInf.toMin HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff inf_right_comm LE.le.trans himp_inf_le le_himp_himp
hnot_anti 📖	mathematical	—	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot	—	hnot_le_comm LE.le.trans hnot_hnot_le
hnot_bot 📖	mathematical	—	HNot.hnot CoheytingAlgebra.toHNot Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BoundedOrder.toOrderBot CoheytingAlgebra.toBoundedOrder Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CoheytingAlgebra.toOrderTop	—	eq_of_forall_ge_iff hnot_le_iff_codisjoint_left codisjoint_bot top_le_iff
hnot_hnot_hnot 📖	mathematical	—	HNot.hnot CoheytingAlgebra.toHNot	—	LE.le.antisymm hnot_hnot_le hnot_anti
hnot_hnot_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot	—	Codisjoint.hnot_le_left codisjoint_hnot_right
hnot_hnot_sdiff_distrib 📖	mathematical	—	HNot.hnot CoheytingAlgebra.toHNot GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra	—	le_antisymm hnot_le_comm LE.le.trans' hnot_anti sdiff_le_inf_hnot hnot_inf_distrib hnot_le_iff_codisjoint_right codisjoint_left_comm le_sdiff_sup sdiff_le_iff hnot_hnot_sup_distrib le_sup_sdiff
hnot_hnot_sup_distrib 📖	mathematical	—	HNot.hnot CoheytingAlgebra.toHNot SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra	—	LE.le.antisymm' LE.le.trans Eq.ge hnot_inf_distrib hnot_anti le_hnot_inf_hnot hnot_le_iff_codisjoint_left codisjoint_assoc codisjoint_hnot_hnot_left_iff codisjoint_left_comm sup_comm codisjoint_hnot_right
hnot_inf_distrib 📖	mathematical	—	HNot.hnot CoheytingAlgebra.toHNot SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sdiff_inf_distrib
hnot_le_comm 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot	—	hnot_le_iff_codisjoint_right hnot_le_iff_codisjoint_left
hnot_le_hnot 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra	HNot.hnot CoheytingAlgebra.toHNot	—	hnot_anti
hnot_le_iff_codisjoint_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot Codisjoint CoheytingAlgebra.toOrderTop	—	hnot_le_iff_codisjoint_right codisjoint_comm
hnot_le_iff_codisjoint_right 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot Codisjoint CoheytingAlgebra.toOrderTop	—	top_sdiff' sdiff_le_iff codisjoint_iff_le_sup
hnot_sdiff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot	—	top_sdiff' sdiff_sdiff sup_idem
hnot_sdiff_comm 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot	—	sdiff_right_comm
hnot_sup_self 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CoheytingAlgebra.toOrderTop	—	Codisjoint.eq_top codisjoint_hnot_left
hnot_top 📖	mathematical	—	HNot.hnot CoheytingAlgebra.toHNot Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop Bot.bot OrderBot.toBot SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderBot CoheytingAlgebra.toBoundedOrder	—	top_sdiff' sdiff_self
inf_compl_eq_bot 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	inf_compl_self
inf_compl_self 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	Disjoint.eq_bot disjoint_compl_right
inf_himp 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_antisymm le_inf inf_le_left inf_comm le_himp_iff le_refl inf_le_inf_left le_himp
inf_himp_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice SemilatticeInf.toMin HImp.himp GeneralizedHeytingAlgebra.toHImp	—	inf_comm le_himp_iff le_refl
inf_sdiff_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	inf_of_le_left sdiff_le
inf_sdiff_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	inf_of_le_right sdiff_le
inf_sdiff_sup_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_of_le_left LE.le.trans sdiff_le le_sup_left
inf_sdiff_sup_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_of_le_left LE.le.trans sdiff_le le_sup_right
le_compl_comm 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	le_compl_iff_disjoint_right le_compl_iff_disjoint_left
le_compl_compl 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	Disjoint.le_compl_right disjoint_compl_right
le_compl_iff_disjoint_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Disjoint HeytingAlgebra.toOrderBot	—	le_compl_iff_disjoint_right disjoint_comm
le_compl_iff_disjoint_right 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Disjoint HeytingAlgebra.toOrderBot	—	himp_bot le_himp_iff disjoint_iff_inf_le
le_compl_iff_le_compl 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	le_compl_comm
le_compl_of_le_compl 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	—	le_compl_comm
le_compl_self 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	le_compl_iff_disjoint_left disjoint_self
le_himp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff inf_le_left
le_himp_comm 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff le_himp_iff'
le_himp_himp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff inf_himp_le
le_himp_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeInf.toMin	—	GeneralizedHeytingAlgebra.le_himp_iff
le_himp_iff' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeInf.toMin	—	le_himp_iff inf_comm
le_himp_iff_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HImp.himp GeneralizedHeytingAlgebra.toHImp	—	le_himp_iff inf_idem
le_hnot_inf_hnot 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin	—	le_inf hnot_anti le_sup_left le_sup_right
le_sdiff_sup 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sup_comm sdiff_le_iff le_refl
le_sup_sdiff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff le_rfl
le_sup_sdiff_sup_sdiff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_sdiff_sdiff_le_sdiff
lt_compl_self 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Compl.compl HeytingAlgebra.toCompl Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup HeytingAlgebra.toOrderBot	—	lt_iff_le_and_ne
ne_compl_self 📖	—	—	—	—	le_compl_self le_of_eq compl_bot
ofDual_compl 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual Compl.compl HeytingAlgebra.toCompl OrderDual.instHeytingAlgebra HNot.hnot CoheytingAlgebra.toHNot	—	—
ofDual_himp 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual HImp.himp GeneralizedHeytingAlgebra.toHImp OrderDual.instGeneralizedHeytingAlgebra CoheytingAlgebra.toGeneralizedCoheytingAlgebra GeneralizedCoheytingAlgebra.toSDiff	—	—
ofDual_hnot 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual HNot.hnot CoheytingAlgebra.toHNot OrderDual.instCoheytingAlgebra Compl.compl HeytingAlgebra.toCompl	—	—
sdiff_bot 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	—	eq_of_forall_ge_iff sdiff_le_iff bot_sup_eq
sdiff_eq_bot_iff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	le_bot_iff sdiff_le_iff sup_bot_eq
sdiff_eq_sdiff_iff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff	—	sup_of_le_left
sdiff_idem 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_sdiff_left sup_idem
sdiff_inf 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sdiff_inf_distrib
sdiff_inf_distrib 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup	—	eq_of_forall_ge_iff sup_le_iff sdiff_le_comm le_inf_iff
sdiff_inf_self_left 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	—	sdiff_inf sdiff_self bot_sup_eq
sdiff_inf_self_right 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	—	sdiff_inf sdiff_self sup_bot_eq
sdiff_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff le_sup_right
sdiff_le_comm 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff sdiff_le_iff'
sdiff_le_hnot 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra GeneralizedCoheytingAlgebra.toSDiff HNot.hnot CoheytingAlgebra.toHNot	—	LE.le.trans_eq sdiff_le_sdiff_right le_top top_sdiff'
sdiff_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	GeneralizedCoheytingAlgebra.sdiff_le_iff
sdiff_le_iff' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sdiff_le_iff sup_comm
sdiff_le_iff_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff sup_idem
sdiff_le_inf_hnot 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra GeneralizedCoheytingAlgebra.toSDiff SemilatticeInf.toMin HNot.hnot CoheytingAlgebra.toHNot	—	le_inf sdiff_le sdiff_le_hnot
sdiff_le_sdiff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	GeneralizedCoheytingAlgebra.toSDiff	—	LE.le.trans sdiff_le_sdiff_right sdiff_le_sdiff_left
sdiff_le_sdiff_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff LE.le.trans le_sup_sdiff sup_le_sup_right
sdiff_le_sdiff_of_sup_le_sup_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup	GeneralizedCoheytingAlgebra.toSDiff	—	sup_sdiff_left_self sdiff_le_sdiff_right
sdiff_le_sdiff_of_sup_le_sup_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeSup.toMax Lattice.toSemilatticeSup	GeneralizedCoheytingAlgebra.toSDiff	—	sup_sdiff_right_self sdiff_le_sdiff_right
sdiff_le_sdiff_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff LE.le.trans le_sup_sdiff
sdiff_ne_sdiff_iff 📖	—	—	—	—	Iff.not sdiff_eq_sdiff_iff
sdiff_right_comm 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_sdiff sup_comm
sdiff_sdiff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice	—	eq_of_forall_ge_iff sup_assoc
sdiff_sdiff_comm 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_right_comm
sdiff_sdiff_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff le_sdiff_sup
sdiff_sdiff_left 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice	—	sdiff_sdiff
sdiff_sdiff_sdiff_le_sdiff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_le_iff sup_left_comm sup_sdiff_self sdiff_sup_self le_sup_left
sdiff_sdiff_self 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	—	sdiff_sdiff_comm sdiff_self bot_sdiff
sdiff_self 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toOrderBot	—	le_bot_iff sdiff_le_iff le_sup_left
sdiff_sup_cancel 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sup_comm sup_sdiff_cancel_right
sdiff_sup_sdiff_cancel 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	LE.le.antisymm' sdiff_triangle sup_le sdiff_le_sdiff_left sdiff_le_sdiff_right
sdiff_sup_sdiff_cancel' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	GeneralizedCoheytingAlgebra.toSDiff	—	LE.le.antisymm' sdiff_triangle sup_le sdiff_inf_self_left sdiff_le_sdiff_left sup_sdiff_self sup_comm
sdiff_sup_self 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sup_comm sup_sdiff_self
sdiff_top 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toOrderTop Bot.bot OrderBot.toBot SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderBot CoheytingAlgebra.toBoundedOrder	—	sdiff_eq_bot_iff le_top
sdiff_triangle 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sdiff_le_iff sup_left_comm LE.le.trans sdiff_sdiff_le le_sup_sdiff
snd_compl 📖	mathematical	—	Compl.compl Prod.instCompl	—	—
snd_himp 📖	mathematical	—	HImp.himp Prod.instHImp	—	—
snd_hnot 📖	mathematical	—	HNot.hnot Prod.instHNot	—	—
snd_sdiff 📖	mathematical	—	Prod.instSDiff	—	—
sup_compl_le_himp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup Compl.compl HeytingAlgebra.toCompl HImp.himp GeneralizedHeytingAlgebra.toHImp	—	sup_le le_himp compl_le_himp
sup_himp_distrib 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice SemilatticeInf.toMin Lattice.toSemilatticeInf	—	eq_of_forall_le_iff le_inf_iff le_himp_comm sup_le_iff
sup_himp_self_left 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice	—	sup_himp_distrib himp_self top_inf_eq
sup_himp_self_right 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice	—	sup_himp_distrib himp_self inf_top_eq
sup_hnot_self 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra HNot.hnot CoheytingAlgebra.toHNot Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CoheytingAlgebra.toOrderTop	—	Codisjoint.eq_top codisjoint_hnot_right
sup_le_of_le_sdiff_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_le LE.le.trans sdiff_le
sup_le_of_le_sdiff_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_le LE.le.trans sdiff_le
sup_sdiff 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice	—	sup_sdiff_distrib
sup_sdiff_cancel' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sup_sdiff_eq_sup sup_of_le_right
sup_sdiff_cancel_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sup_sdiff_cancel' le_rfl
sup_sdiff_distrib 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice	—	eq_of_forall_ge_iff
sup_sdiff_eq_sup 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toSDiff	—	sup_congr_left LE.le.trans sdiff_le le_sup_right le_sup_sdiff sup_le_sup_right
sup_sdiff_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sup_of_le_left sdiff_le
sup_sdiff_left_self 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice	—	sup_comm sup_sdiff_right_self
sup_sdiff_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sup_of_le_right sdiff_le
sup_sdiff_right_self 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice	—	sup_sdiff sdiff_self sup_bot_eq
sup_sdiff_self 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	le_antisymm sup_le_sup_left sdiff_le sup_le le_sup_left le_sup_sdiff
sup_sdiff_self_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sdiff_sup_self
sup_sdiff_self_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedCoheytingAlgebra.toSDiff	—	sup_sdiff_self
toDual_compl 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Compl.compl HeytingAlgebra.toCompl HNot.hnot CoheytingAlgebra.toHNot OrderDual.instCoheytingAlgebra	—	—
toDual_hnot 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual HNot.hnot CoheytingAlgebra.toHNot Compl.compl HeytingAlgebra.toCompl OrderDual.instHeytingAlgebra	—	—
toDual_sdiff 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra HImp.himp GeneralizedHeytingAlgebra.toHImp OrderDual.instGeneralizedHeytingAlgebra	—	—
top_himp 📖	mathematical	—	HImp.himp GeneralizedHeytingAlgebra.toHImp Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice GeneralizedHeytingAlgebra.toOrderTop	—	eq_of_forall_le_iff le_himp_iff inf_top_eq
top_sdiff' 📖	mathematical	—	GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toOrderTop HNot.hnot CoheytingAlgebra.toHNot	—	CoheytingAlgebra.top_sdiff

---

← Back to Index