Basic

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

Statistics

Metric	Count
Definitions `toBiheytingAlgebra`, `toGeneralizedBooleanAlgebra`, `booleanAlgebra`, `generalizedBooleanAlgebra`, `toBooleanAlgebra`, `toGeneralizedCoheytingAlgebra`, `toOrderBot`, `instBooleanAlgebra`, `instBooleanAlgebra`, `instGeneralizedBooleanAlgebra`, `instBooleanAlgebra`, `instGeneralizedBooleanAlgebra`	12
Theorems `toComplementedLattice`, `sdiff_eq_of_sup_eq`, `sdiff_unique`, `compl_eq_iff`, `codisjoint_himp_self_left`, `codisjoint_himp_self_right`, `codisjoint_iff_compl_le_left`, `codisjoint_iff_compl_le_right`, `compl_bijective`, `compl_comp_compl`, `compl_compl`, `compl_eq_bot`, `compl_eq_comm`, `compl_eq_iff_isCompl`, `compl_eq_top`, `compl_himp`, `compl_himp_compl`, `compl_inf`, `compl_inj_iff`, `compl_injective`, `compl_involutive`, `compl_le_compl_iff_le`, `compl_le_iff_compl_le`, `compl_le_of_compl_le`, `compl_le_self`, `compl_lt_compl_iff_lt`, `compl_lt_self`, `compl_sdiff`, `compl_sdiff_compl`, `compl_sup_eq_top`, `compl_surjective`, `disjoint_compl_left_iff`, `disjoint_compl_right_iff`, `disjoint_inf_sdiff`, `disjoint_sdiff_comm`, `disjoint_sdiff_iff_le`, `disjoint_sdiff_sdiff`, `disjoint_sdiff_self_left`, `disjoint_sdiff_self_right`, `eq_compl_comm`, `eq_compl_iff_isCompl`, `eq_of_sdiff_eq_sdiff`, `himp_eq`, `himp_eq_left`, `himp_le`, `himp_le_left`, `himp_ne_right`, `hnot_eq_compl`, `inf_compl_eq_bot'`, `inf_inf_sdiff`, `inf_sdiff`, `inf_sdiff_assoc`, `inf_sdiff_distrib_left`, `inf_sdiff_distrib_right`, `inf_sdiff_eq_bot_iff`, `inf_sdiff_inf`, `inf_sdiff_left_comm`, `inf_sdiff_self_left`, `inf_sdiff_self_right`, `isCompl_compl`, `le_iff_disjoint_sdiff`, `le_iff_eq_sup_sdiff`, `le_sdiff`, `le_sdiff_right`, `sdiff_compl`, `sdiff_eq`, `sdiff_eq_comm`, `sdiff_eq_left`, `sdiff_eq_right`, `sdiff_eq_sdiff_iff_inf_eq_inf`, `sdiff_eq_self_iff_disjoint`, `sdiff_eq_self_iff_disjoint'`, `sdiff_eq_symm`, `sdiff_inf_right_comm`, `sdiff_inf_sdiff`, `sdiff_le_sdiff_iff_le`, `sdiff_lt`, `sdiff_lt_left`, `sdiff_lt_sdiff_right`, `sdiff_ne_right`, `sdiff_sdiff_eq_sdiff_sup`, `sdiff_sdiff_eq_self`, `sdiff_sdiff_left'`, `sdiff_sdiff_right`, `sdiff_sdiff_right'`, `sdiff_sdiff_right_self`, `sdiff_sdiff_sdiff_cancel_left`, `sdiff_sdiff_sdiff_cancel_right`, `sdiff_sdiff_sup_sdiff`, `sdiff_sdiff_sup_sdiff'`, `sdiff_sup`, `sdiff_unique`, `sup_compl_eq_top`, `sup_eq_sdiff_sup_sdiff_sup_inf`, `sup_inf_inf_compl`, `sup_inf_inf_sdiff`, `sup_inf_sdiff`, `sup_lt_of_lt_sdiff_left`, `sup_lt_of_lt_sdiff_right`, `sup_sdiff_inf`, `top_sdiff`	101
Total	113

BooleanAlgebra

Definitions

Name	Category	Theorems
`toBiheytingAlgebra` 📖	CompOp	345 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`, `Set.pairwise_disjoint_Ico_zsmul`, `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`, `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`, `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`, `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`, `Set.offDiag_mono`, `bihimp_le_iff_right`, `TopologicalSpace.Clopens.coe_disjoint`, `MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion`, `BooleanSubalgebra.mk_inf_mk`, `SimpleGraph.disjoint_edgeSet`, `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`, `Set.nsmul_right_monotone`, `compl_image_latticeClosure_eq_of_compl_image_eq_self`, `symmDiff_eq`, `Set.mulIndicator_symmDiff`, `OrderIso.compl_symm_apply`, `hnot_eq_compl`, `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`, `le_iff_atom_le_imp`, `ofBoolAlg_symmDiff`, `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`, `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`, `TopologicalSpace.Clopens.surjective_finset_sup_prod`, `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`, `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`, `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`, `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`, `Set.pairwiseDisjoint_fiber`, `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`, `ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal`, `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`, `Set.covBy_iff_exists_insert`, `Set.disjoint_range_inl_image_inr`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `Set.pairwise_disjoint_Ico_add_zsmul`, `BoundedLatticeHomClass.toBiheytingHomClass`, `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`, `BoolAlg.id_apply`, `Pi.mulSupport_mulSingle_disjoint`, `Set.prod_subset_compl_diagonal_iff_disjoint`, `eq_iff_atom_le_iff`, `toBoolRing_symmDiff`, `bihimp_himp_right`, `bihimp_assoc`, `Set.symmDiff_union_subset`, `Set.pairwise_disjoint_Ioo_intCast`, `FinBoolAlg.forgetToBoolAlgFaithful`, `TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover`, `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`, `BoolAlg.ofHom_apply`, `BoolAlg.forget_map`, `Set.disjoint_univ_pi`, `RingHom.asBoolAlg_toFun`, `bihimp_right_injective`, `Set.pairwiseDisjoint_singleton_iff_injOn`
`toGeneralizedBooleanAlgebra` 📖	CompOp	31 math math: `RingEquiv.asBoolRingAsBoolAlg_apply`, `MeasureTheory.preimage_spanningSetsIndex_singleton`, `toBoolRing_inf`, `BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff`, `biUnion_range_succ_disjointed`, `MeasureTheory.spanningSetsIndex_eq_iff`, `disjointed_eq_inter_compl`, `RingEquiv.asBoolRingAsBoolAlg_symm_apply`, `ofBoolRing_add`, `iUnion_disjointed`, `Finset.diffs_compls_eq_infs`, `ofBoolRing_le_ofBoolRing_iff`, `ofBoolRing_zero`, `biUnion_Iic_disjointed`, `MeasureTheory.NullMeasurableSet.disjointed`, `iSup_disjointed`, `MeasureTheory.mem_disjointed_spanningSetsIndex`, `MeasureTheory.OuterMeasure.isCaratheodory_disjointed`, `ofBoolRing_mul`, `Finset.infs_compls_eq_diffs`, `disjointed_eq_inf_compl`, `Finset.compls_infs_eq_diffs`, `MeasurableSet.disjointed`, `disjointed_subset`, `preimage_find_eq_disjointed`, `MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq`, `toBoolRing_symmDiff`, `MeasureTheory.sum_restrict_disjointed_spanningSets`, `toBoolRing_bot`, `biUnion_Ioc_disjointed_of_monotone`, `MeasureTheory.IsSetRing.disjointed_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toComplementedLattice` 📖	mathematical	—	`ComplementedLattice` `DistribLattice.toLattice` `toDistribLattice` `toBoundedOrder`	—	`isCompl_compl`

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sdiff_eq_of_sup_eq` 📖	mathematical	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`GeneralizedBooleanAlgebra.toSDiff`	—	`inf_eq_right` `LE.le.trans` `le_sup_left` `Eq.le` `sdiff_unique` `eq_bot`
`sdiff_unique` 📖	mathematical	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`GeneralizedBooleanAlgebra.toSDiff`	—	`sdiff_unique` `sup_inf_right` `inf_sup_right` `sup_comm` `inf_sup_self` `inf_comm` `inf_eq_right` `sup_eq_left` `inf_assoc` `eq_bot` `inf_bot_eq`

Function.Injective

Definitions

Name	Category	Theorems
`booleanAlgebra` 📖	CompOp	—
`generalizedBooleanAlgebra` 📖	CompOp	—

GeneralizedBooleanAlgebra

Definitions

Name	Category	Theorems
`toBooleanAlgebra` 📖	CompOp	—
`toGeneralizedCoheytingAlgebra` 📖	CompOp	92 math math: `le_sdiff_right`, `disjoint_sdiff_self_right`, `inf_symmDiff_distrib_right`, `sdiff_symmDiff`, `sdiff_sdiff_sup_sdiff'`, `symmDiff_symmDiff_self'`, `sup_inf_inf_sdiff`, `symmDiff_right_comm`, `Booleanisation.comp_lt_comp`, `symmDiff_left_inj`, `disjoint_symmDiff_inf`, `symmDiff_assoc`, `Finpartition.mem_avoid`, `sdiff_sup`, `sdiff_symmDiff'`, `Fintype.sup_disjointed`, `disjoint_sdiff_comm`, `sdiff_lt_left`, `UV.sup_sdiff_mem_of_mem_compression_of_notMem`, `symmDiff_sdiff_right`, `symmDiff_left_involutive`, `symmDiff_sdiff_left`, `symmDiff_symmDiff_right`, `UV.le_of_mem_compression_of_notMem`, `symmDiff_right_inj`, `sup_eq_sdiff_sup_sdiff_sup_inf`, `disjointed_add_one`, `disjointed_le_id`, `Booleanisation.lift_le_lift`, `partialSups_disjointed`, `sdiff_sdiff_right`, `sdiff_inf_right_comm`, `disjoint_disjointed_of_lt`, `symmDiff_eq_right`, `le_sdiff`, `le_symmDiff_iff_right`, `symmDiff_left_surjective`, `sdiff_sdiff_sup_sdiff`, `inf_symmDiff_distrib_left`, `symmDiff_isAssociative`, `Booleanisation.lift_sdiff_comp`, `Finset.sup_sdiff_right`, `disjointed_le`, `inf_sdiff_assoc`, `Booleanisation.liftLatticeHom_injective`, `Booleanisation.lift_lt_lift`, `sdiff_sdiff_right'`, `symmDiff_symmDiff_left`, `symmDiff_symmDiff_cancel_left`, `Booleanisation.comp_sup_comp`, `Booleanisation.comp_sdiff_lift`, `le_symmDiff_iff_left`, `UV.disjoint_of_mem_compression_of_notMem`, `Booleanisation.lift_lt_comp`, `symmDiff_right_surjective`, `Fintype.exists_disjointed_le`, `disjointed_succ`, `inf_sdiff`, `sdiff_eq_self_iff_disjoint`, `disjointed_apply`, `Booleanisation.comp_inf_comp`, `inf_sdiff_distrib_right`, `symmDiff_left_injective`, `symmDiff_eq_left`, `Booleanisation.lift_inf_lift`, `symmDiff_right_injective`, `sdiff_eq_sdiff_iff_inf_eq_inf`, `disjoint_disjointed`, `sdiff_eq_left`, `inf_sdiff_left_comm`, `symmDiff_eq_sup`, `Booleanisation.lift_sup_lift`, `sdiff_sdiff_right_self`, `sdiff_symmDiff_left`, `symmDiff_left_comm`, `symmDiff_right_involutive`, `Booleanisation.lift_le_comp`, `symmDiff_symmDiff_symmDiff_comm`, `sdiff_eq_self_iff_disjoint'`, `partialSups_add_one_eq_sup_disjointed`, `Finpartition.parts_extendOfLE_of_eq`, `inf_sdiff_distrib_left`, `disjoint_sdiff_self_left`, `sdiff_sdiff_left'`, `symmDiff_symmDiff_cancel_right`, `sup_sdiff_injOn`, `disjointed_partialSups`, `Booleanisation.comp_le_comp`, `Finset.disjiUnion_Iic_disjointed`, `sdiff_symmDiff_right`, `sup_sdiff_symmDiff`, `Finpartition.avoid_parts_val`
`toOrderBot` 📖	CompOp	33 math math: `disjoint_sdiff_self_right`, `disjoint_sdiff_iff_le`, `Finpartition.parts_subset_extendOfLE`, `disjoint_symmDiff_inf`, `le_iff_disjoint_sdiff`, `Finpartition.mem_avoid`, `sup_Ioc_disjointed_of_monotone`, `Fintype.sup_disjointed`, `disjoint_sdiff_comm`, `sdiff_lt_left`, `Finpartition.parts_extendOfLE_of_lt`, `disjoint_disjointed_of_lt`, `le_sdiff`, `le_symmDiff_iff_right`, `Finset.sup_sdiff_right`, `le_symmDiff_iff_left`, `UV.disjoint_of_mem_compression_of_notMem`, `Booleanisation.lift_lt_comp`, `Fintype.exists_disjointed_le`, `disjoint_inf_sdiff`, `sdiff_eq_self_iff_disjoint`, `disjointed_apply`, `disjoint_disjointed`, `sdiff_eq_left`, `symmDiff_eq_sup`, `Booleanisation.lift_le_comp`, `sdiff_eq_self_iff_disjoint'`, `Finpartition.parts_extendOfLE_of_eq`, `disjoint_sdiff_self_left`, `sup_sdiff_injOn`, `Finset.disjiUnion_Iic_disjointed`, `disjoint_sdiff_sdiff`, `Finpartition.avoid_parts_val`

IsCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_eq_iff` 📖	mathematical	`IsCompl` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	`Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_inj_iff` `compl_eq`

OrderDual

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	2 math math: `BoolAlg.dual_map`, `FinBoolAlg.dual_map`

Pi

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	—
`instGeneralizedBooleanAlgebra` 📖	CompOp	—

Prod

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	—
`instGeneralizedBooleanAlgebra` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_himp_self_left` 📖	mathematical	—	`Codisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `CoheytingAlgebra.toOrderTop` `HImp.himp` `BooleanAlgebra.toHImp`	—	`disjoint_sdiff_self_left`
`codisjoint_himp_self_right` 📖	mathematical	—	`Codisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `CoheytingAlgebra.toOrderTop` `HImp.himp` `BooleanAlgebra.toHImp`	—	`disjoint_sdiff_self_right`
`codisjoint_iff_compl_le_left` 📖	mathematical	—	`Codisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `CoheytingAlgebra.toOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `Compl.compl` `BooleanAlgebra.toCompl`	—	`hnot_le_iff_codisjoint_left`
`codisjoint_iff_compl_le_right` 📖	mathematical	—	`Codisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `CoheytingAlgebra.toOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `Compl.compl` `BooleanAlgebra.toCompl`	—	`hnot_le_iff_codisjoint_right`
`compl_bijective` 📖	mathematical	—	`Function.Bijective` `Compl.compl` `BooleanAlgebra.toCompl`	—	`Function.Involutive.bijective` `compl_involutive`
`compl_comp_compl` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_compl`
`compl_compl` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`IsCompl.compl_eq` `IsCompl.symm` `isCompl_compl`
`compl_eq_bot` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `Bot.bot` `BooleanAlgebra.toBot` `Top.top` `BooleanAlgebra.toTop`	—	`IsCompl.compl_eq_iff` `isCompl_top_bot`
`compl_eq_comm` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_eq_iff_isCompl` `eq_compl_iff_isCompl`
`compl_eq_iff_isCompl` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `IsCompl` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	—	`isCompl_compl` `IsCompl.compl_eq`
`compl_eq_top` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `Top.top` `BooleanAlgebra.toTop` `Bot.bot` `BooleanAlgebra.toBot`	—	`IsCompl.compl_eq_iff` `isCompl_bot_top`
`compl_himp` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `HImp.himp` `BooleanAlgebra.toHImp` `BooleanAlgebra.toSDiff`	—	`compl_sdiff`
`compl_himp_compl` 📖	mathematical	—	`HImp.himp` `BooleanAlgebra.toHImp` `Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_sdiff_compl`
`compl_inf` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`hnot_inf_distrib`
`compl_inj_iff` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_injective`
`compl_injective` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`Function.Involutive.injective` `compl_involutive`
`compl_involutive` 📖	mathematical	—	`Function.Involutive` `Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_compl`
`compl_le_compl_iff_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_le_compl` `compl_compl`
`compl_le_iff_compl_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_le_of_compl_le`
`compl_le_of_compl_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	—	`compl_compl` `compl_le_compl`
`compl_le_self` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Top.top` `BooleanAlgebra.toTop`	—	`compl_compl` `le_compl_self`
`compl_lt_compl_iff_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	`lt_iff_lt_of_le_iff_le'` `compl_le_compl_iff_le`
`compl_lt_self` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Top.top` `BooleanAlgebra.toTop`	—	`compl_compl` `lt_compl_self`
`compl_sdiff` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `BooleanAlgebra.toSDiff` `HImp.himp` `BooleanAlgebra.toHImp`	—	`sdiff_eq` `himp_eq` `compl_inf` `compl_compl` `sup_comm`
`compl_sdiff_compl` 📖	mathematical	—	`BooleanAlgebra.toSDiff` `Compl.compl` `BooleanAlgebra.toCompl`	—	`sdiff_compl` `sdiff_eq` `inf_comm`
`compl_sup_eq_top` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `BooleanAlgebra.toDistribLattice` `Compl.compl` `BooleanAlgebra.toCompl` `Top.top` `BooleanAlgebra.toTop`	—	`sup_comm` `sup_compl_eq_top`
`compl_surjective` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`Function.Involutive.surjective` `compl_involutive`
`disjoint_compl_left_iff` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Preorder.toLE` `PartialOrder.toPreorder`	—	`le_compl_iff_disjoint_left` `compl_compl`
`disjoint_compl_right_iff` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Preorder.toLE` `PartialOrder.toPreorder`	—	`le_compl_iff_disjoint_right` `compl_compl`
`disjoint_inf_sdiff` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toOrderBot` `SemilatticeInf.toMin` `GeneralizedBooleanAlgebra.toSDiff`	—	`disjoint_iff_inf_le` `Eq.le` `inf_inf_sdiff`
`disjoint_sdiff_comm` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff`	—	`sdiff_inf_right_comm` `inf_sdiff_assoc`
`disjoint_sdiff_iff_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`Disjoint` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff`	—	`le_of_inf_le_sup_le` `le_trans` `Disjoint.le_bot` `bot_le` `sup_sdiff_cancel_right` `le_imp_le_of_le_of_le` `sup_le_sup` `le_refl` `sdiff_le` `sup_eq_right` `Disjoint.mono_left` `disjoint_sdiff_self_right`
`disjoint_sdiff_sdiff` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff`	—	`disjoint_iff_inf_le` `Eq.le` `sdiff_inf_sdiff`
`disjoint_sdiff_self_left` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff`	—	`disjoint_iff_inf_le` `Eq.le` `inf_sdiff_self_left`
`disjoint_sdiff_self_right` 📖	mathematical	—	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff`	—	`disjoint_iff_inf_le` `Eq.le` `inf_sdiff_self_right`
`eq_compl_comm` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_eq_iff_isCompl` `eq_compl_iff_isCompl`
`eq_compl_iff_isCompl` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `IsCompl` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	—	`IsCompl.symm` `isCompl_compl` `IsCompl.eq_compl`
`eq_of_sdiff_eq_sdiff` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff`	—	—	`sdiff_sdiff_eq_self`
`himp_eq` 📖	mathematical	—	`HImp.himp` `BooleanAlgebra.toHImp` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `BooleanAlgebra.toDistribLattice` `Compl.compl` `BooleanAlgebra.toCompl`	—	`BooleanAlgebra.himp_eq`
`himp_eq_left` 📖	mathematical	—	`HImp.himp` `BooleanAlgebra.toHImp` `Top.top` `BooleanAlgebra.toTop`	—	`Codisjoint.eq_iff` `codisjoint_himp_self_left`
`himp_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HImp.himp` `BooleanAlgebra.toHImp` `Codisjoint` `CoheytingAlgebra.toOrderTop`	—	`le_sdiff` `codisjoint_comm`
`himp_le_left` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HImp.himp` `BooleanAlgebra.toHImp` `Top.top` `BooleanAlgebra.toTop`	—	`codisjoint_self` `Codisjoint.mono_right` `codisjoint_himp_self_right` `LE.le.trans` `le_top` `Eq.ge`
`himp_ne_right` 📖	—	—	—	—	`Iff.not` `himp_eq_left` `not_and_or`
`hnot_eq_compl` 📖	mathematical	—	`HNot.hnot` `BiheytingAlgebra.toHNot` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	—
`inf_compl_eq_bot'` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `BooleanAlgebra.toDistribLattice` `Compl.compl` `BooleanAlgebra.toCompl` `Bot.bot` `BooleanAlgebra.toBot`	—	`bot_unique` `BooleanAlgebra.inf_compl_le_bot`
`inf_inf_sdiff` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`GeneralizedBooleanAlgebra.inf_inf_sdiff`
`inf_sdiff` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	`sdiff_unique` `sup_inf_left` `sup_inf_right` `sup_sdiff_self_right` `inf_sup_right` `inf_sdiff_sup_right` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `inf_sup_self` `sup_inf_inf_sdiff` `inf_comm` `sup_eq_left` `inf_le_inf` `sdiff_le` `inf_sdiff_self_right` `inf_bot_eq` `bot_inf_eq`
`inf_sdiff_assoc` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	`sdiff_unique` `inf_assoc` `inf_sup_left` `sup_inf_sdiff` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `inf_inf_sdiff` `inf_bot_eq`
`inf_sdiff_distrib_left` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff`	—	`sdiff_inf` `sdiff_eq_bot_iff` `inf_le_left` `bot_sup_eq` `inf_sdiff_assoc`
`inf_sdiff_distrib_right` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff`	—	`inf_comm` `inf_sdiff_distrib_left`
`inf_sdiff_eq_bot_iff` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`SemilatticeInf.toMin` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`disjoint_iff` `disjoint_sdiff_iff_le`
`inf_sdiff_inf` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`inf_comm` `inf_inf_sdiff`
`inf_sdiff_left_comm` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff`	—	`inf_comm`
`inf_sdiff_self_left` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`inf_comm` `inf_sdiff_self_right`
`inf_sdiff_self_right` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`sup_inf_sdiff` `inf_sup_right` `inf_comm` `inf_inf_sdiff` `sdiff_inf_sdiff` `bot_sup_eq`
`isCompl_compl` 📖	mathematical	—	`IsCompl` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `BooleanAlgebra.toDistribLattice` `BooleanAlgebra.toBoundedOrder` `Compl.compl` `BooleanAlgebra.toCompl`	—	`IsCompl.of_eq` `inf_compl_eq_bot'` `sup_compl_eq_top`
`le_iff_disjoint_sdiff` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`Disjoint` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff`	—	`disjoint_sdiff_iff_le`
`le_iff_eq_sup_sdiff` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedBooleanAlgebra.toSDiff`	—	`le_antisymm` `sup_inf_sdiff` `sup_le_sup` `inf_eq_right` `le_refl` `le_imp_le_of_le_of_le` `sup_sdiff_left` `le_of_inf_le_sup_le` `inf_sdiff_self_right` `bot_le` `Eq.le` `sup_sdiff_cancel_right`
`le_sdiff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff` `Disjoint` `GeneralizedBooleanAlgebra.toOrderBot`	—	`LE.le.trans` `sdiff_le` `Disjoint.mono_left` `disjoint_sdiff_self_left` `Disjoint.sdiff_eq_left` `sdiff_le_sdiff_right`
`le_sdiff_right` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`disjoint_self` `Disjoint.mono_right` `disjoint_sdiff_self_right` `LE.le.trans` `Eq.le` `bot_le`
`sdiff_compl` 📖	mathematical	—	`BooleanAlgebra.toSDiff` `Compl.compl` `BooleanAlgebra.toCompl` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	—	`sdiff_eq` `compl_compl`
`sdiff_eq` 📖	mathematical	—	`BooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `BooleanAlgebra.toDistribLattice` `Compl.compl` `BooleanAlgebra.toCompl`	—	`BooleanAlgebra.sdiff_eq`
`sdiff_eq_comm` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`GeneralizedBooleanAlgebra.toSDiff`	—	`sdiff_eq_symm`
`sdiff_eq_left` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot`	—	`Disjoint.mono_left` `Eq.ge` `disjoint_sdiff_self_left` `Disjoint.sdiff_eq_left`
`sdiff_eq_right` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`Disjoint.eq_iff` `disjoint_sdiff_self_left`
`sdiff_eq_sdiff_iff_inf_eq_inf` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	`eq_of_inf_eq_sup_eq` `inf_inf_sdiff` `sup_inf_sdiff` `sdiff_inf_self_right` `inf_comm`
`sdiff_eq_self_iff_disjoint` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot`	—	`sdiff_eq_left` `disjoint_comm`
`sdiff_eq_self_iff_disjoint'` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot`	—	`sdiff_eq_left`
`sdiff_eq_symm` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff`	—	—	`sdiff_sdiff_eq_self`
`sdiff_inf_right_comm` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff`	—	`inf_comm` `inf_sdiff_assoc`
`sdiff_inf_sdiff` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toSDiff` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	—	`inf_inf_sdiff` `sup_inf_sdiff` `inf_sup_left` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `inf_idem` `inf_sup_right` `inf_comm` `bot_sup_eq` `inf_of_le_right`
`sdiff_le_sdiff_iff_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`GeneralizedBooleanAlgebra.toSDiff`	—	`sdiff_sdiff_eq_self` `sdiff_le_sdiff_left`
`sdiff_lt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`Preorder.toLT` `GeneralizedBooleanAlgebra.toSDiff`	—	`LE.le.lt_of_ne` `sdiff_le` `disjoint_iff` `sdiff_eq_left` `inf_eq_right`
`sdiff_lt_left` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff` `Disjoint` `GeneralizedBooleanAlgebra.toOrderBot`	—	`lt_iff_le_and_ne` `sdiff_eq_self_iff_disjoint` `sdiff_le`
`sdiff_lt_sdiff_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `Preorder.toLE`	`GeneralizedBooleanAlgebra.toSDiff`	—	`LE.le.lt_of_not_ge` `sdiff_le_sdiff_right` `LT.lt.le` `LT.lt.not_ge` `LE.le.trans` `le_sdiff_sup` `sup_le_of_le_sdiff_right`
`sdiff_ne_right` 📖	—	—	—	—	`Iff.not` `sdiff_eq_right` `not_and_or`
`sdiff_sdiff_eq_sdiff_sup` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sdiff_sdiff_right'` `inf_eq_right`
`sdiff_sdiff_eq_self` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`GeneralizedBooleanAlgebra.toSDiff`	—	`sdiff_sdiff_right_self` `inf_of_le_right`
`sdiff_sdiff_left'` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	`sdiff_sdiff_left` `sdiff_sup`
`sdiff_sdiff_right` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sup_comm` `inf_comm` `inf_assoc` `sup_inf_inf_sdiff` `sdiff_unique` `sup_inf_right` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `sup_inf_self` `sup_sdiff_left` `sup_assoc` `sup_inf_left` `inf_sup_right` `inf_sdiff_sup_right` `inf_sup_left` `sup_inf_sdiff` `inf_sup_self` `inf_sdiff_self_left` `bot_inf_eq` `inf_bot_eq` `bot_sup_eq` `inf_sdiff_left` `inf_sdiff_self_right`
`sdiff_sdiff_right'` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sdiff_sdiff_right` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `sup_inf_inf_sdiff` `sup_comm` `inf_comm`
`sdiff_sdiff_right_self` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	`sdiff_sdiff_right` `inf_idem` `sdiff_self` `bot_sup_eq`
`sdiff_sdiff_sdiff_cancel_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`GeneralizedBooleanAlgebra.toSDiff`	—	`LE.le.antisymm` `sdiff_sdiff_sdiff_le_sdiff` `Disjoint.le_sdiff_of_le_left` `Disjoint.mono_left` `sdiff_le` `disjoint_sdiff_self_right` `sdiff_le_sdiff_right`
`sdiff_sdiff_sdiff_cancel_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`GeneralizedBooleanAlgebra.toSDiff`	—	`le_antisymm_iff` `sdiff_le_comm` `sdiff_sdiff_sdiff_le_sdiff` `Disjoint.le_sdiff_of_le_left` `Disjoint.mono_right` `sdiff_le` `disjoint_sdiff_self_left` `sdiff_le_sdiff_left`
`sdiff_sdiff_sup_sdiff` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sdiff_sup` `sdiff_sdiff_right` `sup_inf_left` `sup_comm` `sup_inf_sdiff` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `inf_idem`
`sdiff_sdiff_sup_sdiff'` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sdiff_sup` `sdiff_sdiff_right` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `sup_inf_right`
`sdiff_sup` 📖	mathematical	—	`GeneralizedBooleanAlgebra.toSDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sdiff_unique` `sup_inf_left` `inf_sup_left` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `sup_inf_sdiff` `sup_inf_self` `inf_idem` `inf_sup_right` `inf_inf_sdiff` `bot_inf_eq` `bot_sup_eq` `inf_comm` `inf_bot_eq`
`sdiff_unique` 📖	mathematical	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `Bot.bot` `GeneralizedBooleanAlgebra.toBot`	`GeneralizedBooleanAlgebra.toSDiff`	—	`eq_of_inf_eq_sup_eq` `inf_comm` `inf_inf_sdiff` `sup_comm` `sup_inf_sdiff`
`sup_compl_eq_top` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `BooleanAlgebra.toDistribLattice` `Compl.compl` `BooleanAlgebra.toCompl` `Top.top` `BooleanAlgebra.toTop`	—	`top_unique` `BooleanAlgebra.top_le_sup_compl`
`sup_eq_sdiff_sup_sdiff_sup_inf` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sup_inf_left` `instAssociativeMax_mathlib` `instCommutativeMax_mathlib` `instIdempotentOpMax_mathlib` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib` `sup_of_le_right` `sup_sdiff_self` `sdiff_sup_self` `inf_of_le_left`
`sup_inf_inf_compl` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `Compl.compl` `BooleanAlgebra.toCompl`	—	`sdiff_eq` `sup_inf_sdiff`
`sup_inf_inf_sdiff` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedBooleanAlgebra.toSDiff`	—	`inf_assoc` `sup_inf_right` `sup_inf_sdiff` `inf_sup_right` `inf_sdiff_left`
`sup_inf_sdiff` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedBooleanAlgebra.toSDiff`	—	`GeneralizedBooleanAlgebra.sup_inf_sdiff`
`sup_lt_of_lt_sdiff_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff` `Preorder.toLE`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sup_sdiff_cancel_right` `LE.le.lt_of_not_ge` `sup_le_sup_left` `LT.lt.le` `LT.lt.not_ge` `sdiff_idem` `LE.le.trans` `sdiff_le_sdiff_of_sup_le_sup_left` `sdiff_le`
`sup_lt_of_lt_sdiff_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toSDiff` `Preorder.toLE`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sdiff_sup_cancel` `lt_of_le_not_ge` `le_imp_le_of_le_of_le` `sup_le_sup` `le_of_lt` `le_refl` `LT.lt.not_ge` `sdiff_idem` `LE.le.trans` `sdiff_le_sdiff_of_sup_le_sup_right` `sdiff_le`
`sup_sdiff_inf` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `GeneralizedBooleanAlgebra.toDistribLattice` `GeneralizedBooleanAlgebra.toSDiff` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sup_comm` `sup_inf_sdiff`
`top_sdiff` 📖	mathematical	—	`BooleanAlgebra.toSDiff` `Top.top` `BooleanAlgebra.toTop` `Compl.compl` `BooleanAlgebra.toCompl`	—	`top_sdiff'`

---

← Back to Index