Set

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

Statistics

Metric	Count
Definitions instBooleanAlgebra, ite	2
Theorems subset_compl_left, subset_compl_right, diff_ssubset_of_nonempty, disjoint_compl_left, disjoint_compl_right, compl_def, compl_diff, compl_empty, compl_empty_iff, compl_eq_univ_diff, compl_inter, compl_inter_self, compl_ne_eq_singleton, compl_ne_univ, compl_setOf, compl_singleton_eq, compl_subset_comm, compl_subset_compl, compl_subset_compl_of_subset, compl_subset_iff_union, compl_union, compl_union_self, compl_univ, compl_univ_iff, diff_compl, diff_diff, diff_diff_cancel_left, diff_diff_comm, diff_diff_eq_sdiff_union, diff_diff_right, diff_diff_right_self, diff_empty, diff_eq_compl_inter, diff_eq_empty, diff_insert_of_notMem, diff_inter, diff_inter_diff, diff_inter_distrib_right, diff_inter_right_comm, diff_inter_self, diff_inter_self_eq_diff, diff_nonempty, diff_self, diff_self_inter, diff_singleton_eq_self, diff_singleton_ssubset, diff_singleton_subset_iff, diff_ssubset_left_iff, diff_subset, diff_subset_comm, diff_subset_compl, diff_subset_diff, diff_subset_diff_iff_subset, diff_subset_diff_left, diff_subset_diff_right, diff_subset_iff, diff_union_diff_cancel, diff_union_diff_cancel', diff_union_inter, diff_union_of_subset, diff_union_self, diff_univ, disjoint_compl_left_iff_subset, disjoint_compl_right_iff_subset, disjoint_of_subset_iff_left_eq_empty, disjoint_sdiff_inter, disjoint_sdiff_left, disjoint_sdiff_right, empty_diff, inl_compl_union_inr_compl, insert_diff_insert, insert_diff_of_mem, insert_diff_of_notMem, insert_diff_self_of_mem, insert_diff_self_of_notMem, insert_diff_singleton, insert_diff_singleton_comm, insert_diff_subset, insert_erase_invOn, inter_compl_nonempty_iff, inter_compl_self, inter_diff_assoc, inter_diff_distrib_left, inter_diff_distrib_right, inter_diff_right_comm, inter_diff_self, inter_eq_compl_compl_union_compl, inter_sdiff_left_comm, inter_subset, inter_subset_ite, inter_union_compl, inter_union_diff, ite_compl, ite_diff_self, ite_empty, ite_empty_left, ite_empty_right, ite_eq_of_subset_left, ite_eq_of_subset_right, ite_inter, ite_inter_compl_self, ite_inter_inter, ite_inter_of_inter_eq, ite_inter_self, ite_left, ite_mono, ite_right, ite_same, ite_subset_union, ite_univ, mem_compl, mem_compl_singleton_iff, mem_diff_singleton, mem_diff_singleton_empty, mem_of_mem_diff, nonempty_compl, nonempty_compl_of_nontrivial, notMem_compl_iff, notMem_diff_of_mem, notMem_of_mem_compl, notMem_of_mem_diff, pair_diff_left, pair_diff_right, sdiff_inter_right_comm, sdiff_sep_self, ssubset_iff_sdiff_singleton, subset_compl_comm, subset_compl_iff_disjoint_left, subset_compl_iff_disjoint_right, subset_compl_singleton_iff, subset_diff, subset_diff_singleton, subset_diff_union, subset_insert_diff_singleton, subset_insert_iff, subset_inter_union_compl_left, subset_inter_union_compl_right, subset_ite, subset_union_compl_iff_inter_subset, union_compl_self, union_diff_cancel, union_diff_cancel', union_diff_cancel_left, union_diff_cancel_right, union_diff_distrib, union_diff_left, union_diff_right, union_diff_self, union_eq_compl_compl_inter_compl, union_eq_diff_union_diff_union_inter, union_inter_compl_left_subset, union_inter_compl_right_subset	152
Total	154

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subset_compl_left 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	Set.instHasSubset Compl.compl Set.instCompl	—	Set.subset_compl_iff_disjoint_left
subset_compl_right 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	Set.instHasSubset Compl.compl Set.instCompl	—	Set.subset_compl_iff_disjoint_right

HasSubset.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diff_ssubset_of_nonempty 📖	mathematical	Set Set.instHasSubset Set.Nonempty	Set.instHasSSubset Set.instSDiff	—	Set.inter_eq_self_of_subset_right
disjoint_compl_left 📖	mathematical	Set Set.instHasSubset	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Compl.compl Set.instCompl	—	Set.disjoint_compl_left_iff_subset
disjoint_compl_right 📖	mathematical	Set Set.instHasSubset	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Compl.compl Set.instCompl	—	Set.disjoint_compl_right_iff_subset

Set

Definitions

Name	Category	Theorems
instBooleanAlgebra 📖	CompOp	200 math math: pairwiseDisjoint_range_iff, pairwise_disjoint_Ioc_zpow, pairwise_disjoint_Ioo_add_zsmul, inter_symmDiff_distrib_left, functorToTypes_obj, Finite.inf_of_right, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, Sym2.disjoint_diagSet_fromRel, disjoint_compl_left_iff_subset, pairwise_disjoint_Ico_zsmul, SSet.degenerate_eq_top_of_hasDimensionLT, pairwise_disjoint_Ioo_mul_zpow, MeasureTheory.preimage_spanningSetsIndex_singleton, sdiff_singleton_wcovBy, image_symmDiff, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, disjoint_of_subset_iff_left_eq_empty, BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, SetRel.core_mono, IsClopen.himp, toFinset_symmDiff, isCompl_range_some_none, biUnion_range_succ_disjointed, indicator_symmDiff, pairwise_disjoint_fiber, symmDiff_def, covBy_iff_exists_sdiff_singleton, instWellFoundedLTSubtypeSetFinite, SetRel.prod_comp_prod, disjoint_image_left, sdiff_singleton_covBy, MeasureTheory.spanningSetsIndex_eq_iff, Types.monoOverEquivalenceSet_inverse_map, SSet.Subcomplex.degenerate_eq_top_iff, pairwise_disjoint_Ioc_zsmul, disjointed_eq_inter_compl, subset_compl_iff_disjoint_right, mem_symmDiff, SetRel.image_core_gc, disjoint_sdiff_inter, pairwise_disjoint_Ioo_add_intCast, covBy_insert, HasSubset.Subset.disjoint_compl_right, iUnion_disjointed, disjoint_of_sSup_disjoint, SSet.nonDegenerate_eq_bot_of_hasDimensionLT, SimpleGraph.edgeSet_eq_iff, pairwise_disjoint_Ioc_add_zsmul, disjoint_powerset_insert, disjoint_toFinset, pairwise_disjoint_Ioc_mul_zpow, pairwise_disjoint_Ico_mul_zpow, offDiag_mono, Topology.IsConstructible.himp, Sylow.orbit_eq_top, SimpleGraph.disjoint_edgeSet, SSet.hasDimensionLT_iff, MeasurableSet.coe_bot, union_symmDiff_subset, SSet.skeleton_obj_eq_top, pairwise_disjoint_Ico_add_intCast, subset_diff, Int.isCompl_even_odd, CategoryTheory.Subfunctor.Subpresheaf.bot_obj, Finite.toFinset_symmDiff, nsmul_right_monotone, mulIndicator_symmDiff, MeasurableSet.bihimp, disjoint_prod, Subgroup.closure_mul_image_mul_eq_top, indicator_eq_zero', disjoint_image_iff, disjoint_pi, MeasurableSet.himp, MvPolynomial.zeroLocus_bot, indicator_eq_zero, empty_covBy_singleton, disjoint_of_sSup_disjoint_of_le_of_le, ContinuousMap.sublattice_closure_eq_top, fintypeToFinBoolAlgOp_map, Definable.himp, pow_right_monotone, typeToBoolAlgOp_map, MeasurableSet.coe_himp, apply_indicator_symmDiff, disjoint_compl_right_iff_subset, pairwise_disjoint_Ioo_zpow, Finite.inf_of_left, gc_Ici_sInf, disjoint_image_image, symmDiff_subset_union, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, biUnion_Iic_disjointed, CategoryTheory.Subfunctor.Subpresheaf.top_obj, zero_mem_neg_add_iff, pairwise_disjoint_Ioc_intCast, subset_compl_iff_disjoint_left, Types.monoOverEquivalenceSet_functor_map, pairwise_disjoint_Ioo_zsmul, CategoryTheory.Limits.Types.isPushout_of_bicartSq, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, SimpleGraph.fromEdgeSet_disjoint, MeasureTheory.NullMeasurableSet.disjointed, SetRel.image_mono, Function.Injective.image_strictMono, CategoryTheory.Subfunctor.bot_obj, locallyFinsuppWithin.logCounting_divisor, disjoint_image_right, Types.monoOverEquivalenceSet_functor_obj, MeasureTheory.mem_disjointed_spanningSetsIndex, Function.mulSupport_disjoint_iff, pairwise_disjoint_Ioc_add_intCast, eq_top_of_card_le_of_finite, Finite.symmDiff_congr, inter_symmDiff_distrib_right, SetRel.preimage_mono, Finset.coe_symmDiff, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, mulIndicator_eq_one', Function.support_disjoint_iff, isCompl_range_inl_range_inr, MeasureTheory.OuterMeasure.isCaratheodory_disjointed, one_notMem_inv_mul_iff, preimage_eq_empty_iff, SSet.horn_obj_zero, disjoint_image_inl_image_inr, disjoint_sdiff_left, TopologicalSpace.Clopens.coe_himp, gc_sSup_Iic, pairwise_disjoint_Ico_zpow, SSet.skeletonOfMono_obj_eq_top, disjoint_preimage_iff, apply_mulIndicator_symmDiff, SimpleGraph.IsCompleteBetween.disjoint, disjoint_sdiff_right, zero_notMem_sub_iff, one_notMem_div_iff, Finite.disjoint_toFinset, MeasurableSet.disjointed, pairwiseDisjoint_range_singleton, SSet.HasDimensionLT.degenerate_eq_top, MeasurableSet.coe_top, Finite.symmDiff, disjoint_diagonal_offDiag, SetRel.gc_leftDual_rightDual, symmDiff_eq_empty, mulIndicator_eq_one, Types.monoOverEquivalenceSet_inverse_obj, one_mem_div_iff, disjointed_subset, pairwise_disjoint_Ico_intCast, MvPolynomial.zeroLocus_top, SimpleGraph.disjoint_fromEdgeSet, CategoryTheory.Subfunctor.top_obj, pairwiseDisjoint_fiber, zero_notMem_neg_add_iff, disjoint_image_inl_range_inr, subsingleton_setOf_mem_iff_pairwise_disjoint, pairwiseDisjoint_image_right_iff, Types.monoOverEquivalenceSet_unitIso, FirstOrder.Language.DefinableSet.coe_himp, symmDiff_nonempty, preimage_symmDiff, functorToTypes_map, Finite.sup, Nat.isCompl_even_odd, subset_image_symmDiff, zero_mem_sub_iff, preimage_find_eq_disjointed, pairwiseDisjoint_image_left_iff, monotone_image, wcovBy_insert, instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, covBy_iff_exists_insert, disjoint_range_inl_image_inr, pairwise_disjoint_Ico_add_zsmul, CompactSpace.elim_nhds_subcover, Types.monoOverEquivalenceSet_counitIso, MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq, fintypeToFinBoolAlgOp_obj, PMF.support_uniformOfFintype, Pi.mulSupport_mulSingle_disjoint, prod_subset_compl_diagonal_iff_disjoint, irreducibleSpace_def, Submodule.IsPrimary.mem_or_mem, MeasureTheory.sum_restrict_disjointed_spanningSets, symmDiff_union_subset, pairwise_disjoint_Ioo_intCast, biUnion_Ioc_disjointed_of_monotone, TopologicalSpace.CompactOpens.coe_himp, MeasureTheory.IsSetRing.disjointed_mem, Function.disjoint_support_iff, union_symmDiff_union_subset, one_mem_inv_mul_iff, disjoint_univ_pi, typeToBoolAlgOp_obj, pairwiseDisjoint_singleton_iff_injOn
ite 📖	CompOp	38 math math: PartialEquiv.piecewise_source, mulIndicator_preimage, subset_ite, ite_inter_closure_compl_eq_of_inter_frontier_eq, ite_empty_left, EqOn.piecewise_ite', ite_same, PartialEquiv.IsImage.leftInvOn_piecewise, MeasurableSet.ite, continuousOn_piecewise_ite', ite_compl, ite_right, ite_empty_right, ite_eq_of_subset_right, continuousOn_piecewise_ite, preimage_ite, PartialEquiv.piecewise_target, EqOn.piecewise_ite, ite_diff_self, inter_subset_ite, OpenPartialHomeomorph.IsImage.leftInvOn_piecewise, ite_subset_union, indicator_preimage, piecewise_preimage, ite_inter_compl_self, MapsTo.piecewise_ite, IsOpen.ite', ite_univ, ite_left, ite_inter_of_inter_eq, ite_eq_of_subset_left, IsOpen.ite, ite_empty, ite_inter_inter, ite_mono, ite_inter, ite_inter_self, ite_inter_closure_eq_of_inter_frontier_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_def 📖	mathematical	—	Compl.compl Set instCompl setOf instMembership	—	—
compl_diff 📖	mathematical	—	Compl.compl Set instCompl instSDiff instUnion	—	compl_sdiff himp_eq
compl_empty 📖	mathematical	—	Compl.compl Set instCompl instEmptyCollection univ	—	compl_bot
compl_empty_iff 📖	mathematical	—	Compl.compl Set instCompl instEmptyCollection univ	—	compl_eq_bot
compl_eq_univ_diff 📖	mathematical	—	Compl.compl Set instCompl instSDiff univ	—	top_sdiff
compl_inter 📖	mathematical	—	Compl.compl Set instCompl instInter instUnion	—	compl_inf
compl_inter_self 📖	mathematical	—	Set instInter Compl.compl instCompl instEmptyCollection	—	compl_inf_eq_bot
compl_ne_eq_singleton 📖	mathematical	—	Compl.compl Set instCompl setOf instSingletonSet	—	compl_compl
compl_ne_univ 📖	mathematical	—	Nonempty	—	Iff.not compl_univ_iff nonempty_iff_ne_empty
compl_setOf 📖	mathematical	—	Compl.compl Set instCompl setOf	—	—
compl_singleton_eq 📖	mathematical	—	Compl.compl Set instCompl instSingletonSet setOf	—	—
compl_subset_comm 📖	mathematical	—	Set instHasSubset Compl.compl instCompl	—	compl_le_iff_compl_le
compl_subset_compl 📖	mathematical	—	Set instHasSubset Compl.compl instCompl	—	compl_le_compl_iff_le
compl_subset_compl_of_subset 📖	mathematical	Set instHasSubset	Compl.compl instCompl	—	compl_subset_compl
compl_subset_iff_union 📖	mathematical	—	Set instHasSubset Compl.compl instCompl instUnion univ	—	eq_univ_iff_forall
compl_union 📖	mathematical	—	Compl.compl Set instCompl instUnion instInter	—	compl_sup
compl_union_self 📖	mathematical	—	Set instUnion Compl.compl instCompl univ	—	union_comm union_compl_self
compl_univ 📖	mathematical	—	Compl.compl Set instCompl univ instEmptyCollection	—	compl_top
compl_univ_iff 📖	mathematical	—	Compl.compl Set instCompl univ instEmptyCollection	—	compl_eq_top
diff_compl 📖	mathematical	—	Set instSDiff Compl.compl instCompl instInter	—	sdiff_compl
diff_diff 📖	mathematical	—	Set instSDiff instUnion	—	sdiff_sdiff_left
diff_diff_cancel_left 📖	mathematical	Set instHasSubset	instSDiff	—	sdiff_sdiff_eq_self
diff_diff_comm 📖	mathematical	—	Set instSDiff	—	sdiff_sdiff_comm
diff_diff_eq_sdiff_union 📖	mathematical	Set instHasSubset	instSDiff instUnion	—	sdiff_sdiff_eq_sdiff_sup
diff_diff_right 📖	mathematical	—	Set instSDiff instUnion instInter	—	sdiff_sdiff_right'
diff_diff_right_self 📖	mathematical	—	Set instSDiff instInter	—	sdiff_sdiff_right_self
diff_empty 📖	mathematical	—	Set instSDiff instEmptyCollection	—	sdiff_bot
diff_eq_compl_inter 📖	mathematical	—	Set instSDiff instInter Compl.compl instCompl	—	diff_eq inter_comm
diff_eq_empty 📖	mathematical	—	Set instSDiff instEmptyCollection instHasSubset	—	sdiff_eq_bot_iff
diff_insert_of_notMem 📖	mathematical	Set instMembership	instSDiff instInsert	—	—
diff_inter 📖	mathematical	—	Set instSDiff instInter instUnion	—	sdiff_inf
diff_inter_diff 📖	mathematical	—	Set instInter instSDiff instUnion	—	sdiff_sup
diff_inter_distrib_right 📖	mathematical	—	Set instSDiff instInter	—	inf_sdiff
diff_inter_right_comm 📖	mathematical	—	Set instInter instSDiff	—	diff_eq inter_right_comm
diff_inter_self 📖	mathematical	—	Set instInter instSDiff instEmptyCollection	—	inf_sdiff_self_left
diff_inter_self_eq_diff 📖	mathematical	—	Set instSDiff instInter	—	sdiff_inf_self_right
diff_nonempty 📖	mathematical	—	Nonempty Set instSDiff instHasSubset	—	inter_compl_nonempty_iff
diff_self 📖	mathematical	—	Set instSDiff instEmptyCollection	—	sdiff_self
diff_self_inter 📖	mathematical	—	Set instSDiff instInter	—	sdiff_inf_self_left
diff_singleton_eq_self 📖	mathematical	Set instMembership	instSDiff instSingletonSet	—	sdiff_eq_self_iff_disjoint
diff_singleton_ssubset 📖	mathematical	—	Set instHasSSubset instSDiff instSingletonSet instMembership	—	—
diff_singleton_subset_iff 📖	mathematical	—	Set instHasSubset instSDiff instSingletonSet instInsert	—	union_singleton union_comm diff_subset_iff
diff_ssubset_left_iff 📖	mathematical	—	Set instHasSSubset instSDiff Nonempty instInter	—	sdiff_lt_left not_disjoint_iff_nonempty_inter inter_comm
diff_subset 📖	mathematical	—	Set instHasSubset instSDiff	—	sdiff_le
diff_subset_comm 📖	mathematical	—	Set instHasSubset instSDiff	—	sdiff_le_comm
diff_subset_compl 📖	mathematical	—	Set instHasSubset instSDiff Compl.compl instCompl	—	inter_subset_left diff_eq_compl_inter
diff_subset_diff 📖	mathematical	Set instHasSubset	instSDiff	—	sdiff_le_sdiff
diff_subset_diff_iff_subset 📖	mathematical	Set instHasSubset	instSDiff	—	sdiff_le_sdiff_iff_le
diff_subset_diff_left 📖	mathematical	Set instHasSubset	instSDiff	—	sdiff_le_sdiff_right
diff_subset_diff_right 📖	mathematical	Set instHasSubset	instSDiff	—	sdiff_le_sdiff_left
diff_subset_iff 📖	mathematical	—	Set instHasSubset instSDiff instUnion	—	sdiff_le_iff
diff_union_diff_cancel 📖	mathematical	Set instHasSubset	instUnion instSDiff	—	sdiff_sup_sdiff_cancel
diff_union_diff_cancel' 📖	mathematical	Set instHasSubset instInter instUnion	instSDiff	—	sdiff_sup_sdiff_cancel'
diff_union_inter 📖	mathematical	—	Set instUnion instSDiff instInter	—	union_comm sup_inf_sdiff
diff_union_of_subset 📖	mathematical	Set instHasSubset	instUnion instSDiff	—	Subset.antisymm union_subset diff_subset subset_diff_union
diff_union_self 📖	mathematical	—	Set instUnion instSDiff	—	sdiff_sup_self
diff_univ 📖	mathematical	—	Set instSDiff univ instEmptyCollection	—	diff_eq_empty subset_univ
disjoint_compl_left_iff_subset 📖	mathematical	—	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Compl.compl instCompl instHasSubset	—	disjoint_compl_left_iff
disjoint_compl_right_iff_subset 📖	mathematical	—	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Compl.compl instCompl instHasSubset	—	disjoint_compl_right_iff
disjoint_of_subset_iff_left_eq_empty 📖	mathematical	Set instHasSubset	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra instEmptyCollection	—	disjoint_of_le_iff_left_eq_bot
disjoint_sdiff_inter 📖	mathematical	—	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra instSDiff instInter	—	disjoint_of_subset_right inter_subset_right disjoint_sdiff_left
disjoint_sdiff_left 📖	mathematical	—	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra instSDiff	—	disjoint_sdiff_self_left
disjoint_sdiff_right 📖	mathematical	—	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra instSDiff	—	disjoint_sdiff_self_right
empty_diff 📖	mathematical	—	Set instSDiff instEmptyCollection	—	bot_sdiff
inl_compl_union_inr_compl 📖	mathematical	—	Set instUnion image Compl.compl instCompl	—	—
insert_diff_insert 📖	mathematical	—	Set instInsert instSDiff	—	union_singleton diff_diff insert_diff_singleton
insert_diff_of_mem 📖	mathematical	Set instMembership	instSDiff instInsert	—	—
insert_diff_of_notMem 📖	mathematical	Set instMembership	instSDiff instInsert	—	—
insert_diff_self_of_mem 📖	mathematical	Set instMembership	instInsert instSDiff instSingletonSet	—	ext
insert_diff_self_of_notMem 📖	mathematical	Set instMembership	instSDiff instInsert instSingletonSet	—	ext insert_diff_of_mem
insert_diff_singleton 📖	mathematical	—	Set instInsert instSDiff instSingletonSet	—	union_diff_self
insert_diff_singleton_comm 📖	mathematical	—	Set instInsert instSDiff instSingletonSet	—	union_diff_distrib diff_singleton_eq_self Iff.not mem_singleton_iff
insert_diff_subset 📖	mathematical	—	Set instHasSubset instSDiff instInsert	—	—
insert_erase_invOn 📖	mathematical	—	InvOn Set instInsert instSDiff instSingletonSet setOf instMembership	—	insert_diff_self_of_mem insert_diff_self_of_notMem
inter_compl_nonempty_iff 📖	mathematical	—	Nonempty Set instInter Compl.compl instCompl instHasSubset	—	not_subset
inter_compl_self 📖	mathematical	—	Set instInter Compl.compl instCompl instEmptyCollection	—	inf_compl_eq_bot
inter_diff_assoc 📖	mathematical	—	Set instSDiff instInter	—	inf_sdiff_assoc
inter_diff_distrib_left 📖	mathematical	—	Set instInter instSDiff	—	inf_sdiff_distrib_left
inter_diff_distrib_right 📖	mathematical	—	Set instInter instSDiff	—	inf_sdiff_distrib_right
inter_diff_right_comm 📖	mathematical	—	Set instSDiff instInter	—	diff_eq inter_right_comm
inter_diff_self 📖	mathematical	—	Set instInter instSDiff instEmptyCollection	—	inf_sdiff_self_right
inter_eq_compl_compl_union_compl 📖	mathematical	—	Set instInter Compl.compl instCompl instUnion	—	ext and_iff_not_or_not
inter_sdiff_left_comm 📖	mathematical	—	Set instInter instSDiff	—	inf_sdiff_left_comm
inter_subset 📖	mathematical	—	Set instHasSubset instInter instUnion Compl.compl instCompl	—	imp_iff_not_or
inter_subset_ite 📖	mathematical	—	Set instHasSubset instInter ite	—	ite_mono inter_subset_left inter_subset_right ite_same
inter_union_compl 📖	mathematical	—	Set instUnion instInter Compl.compl instCompl	—	inter_union_diff
inter_union_diff 📖	mathematical	—	Set instUnion instInter instSDiff	—	sup_inf_sdiff
ite_compl 📖	mathematical	—	ite Compl.compl Set instCompl	—	ite.eq_1 diff_compl union_comm diff_eq
ite_diff_self 📖	mathematical	—	Set instSDiff ite	—	ite_inter_compl_self
ite_empty 📖	mathematical	—	ite Set instEmptyCollection	—	inter_empty diff_empty empty_union
ite_empty_left 📖	mathematical	—	ite Set instEmptyCollection instSDiff	—	empty_inter empty_union
ite_empty_right 📖	mathematical	—	ite Set instEmptyCollection instInter	—	empty_diff union_empty
ite_eq_of_subset_left 📖	mathematical	Set instHasSubset	ite instUnion instSDiff	—	ext
ite_eq_of_subset_right 📖	mathematical	Set instHasSubset	ite instUnion instInter	—	ext
ite_inter 📖	mathematical	—	ite Set instInter	—	ite_inter_inter ite_same
ite_inter_compl_self 📖	mathematical	—	Set instInter ite Compl.compl instCompl	—	ite_compl ite_inter_self
ite_inter_inter 📖	mathematical	—	ite Set instInter	—	ext
ite_inter_of_inter_eq 📖	mathematical	Set instInter	ite	—	ite_inter ite_same
ite_inter_self 📖	mathematical	—	Set instInter ite	—	ite.eq_1 union_inter_distrib_right diff_inter_self inter_assoc inter_self union_empty
ite_left 📖	mathematical	—	ite Set instUnion	—	inter_self union_diff_self
ite_mono 📖	mathematical	Set instHasSubset	ite	—	union_subset_union inter_subset_inter_left
ite_right 📖	mathematical	—	ite Set instInter	—	sdiff_self union_empty
ite_same 📖	mathematical	—	ite	—	inter_union_diff
ite_subset_union 📖	mathematical	—	Set instHasSubset ite instUnion	—	union_subset_union inter_subset_left diff_subset
ite_univ 📖	mathematical	—	ite univ	—	inter_univ diff_univ union_empty
mem_compl 📖	mathematical	Set instMembership	Compl.compl instCompl	—	—
mem_compl_singleton_iff 📖	mathematical	—	Set instMembership Compl.compl instCompl instSingletonSet	—	—
mem_diff_singleton 📖	mathematical	—	Set instMembership instSDiff instSingletonSet	—	—
mem_diff_singleton_empty 📖	mathematical	—	Set instMembership instSDiff instSingletonSet instEmptyCollection Nonempty	—	mem_diff_singleton nonempty_iff_ne_empty
mem_of_mem_diff 📖	—	Set instMembership instSDiff	—	—	—
nonempty_compl 📖	mathematical	—	Nonempty Compl.compl Set instCompl	—	ne_univ_iff_exists_notMem
nonempty_compl_of_nontrivial 📖	mathematical	—	Nonempty Compl.compl Set instCompl instSingletonSet	—	exists_ne
notMem_compl_iff 📖	mathematical	—	Set instMembership Compl.compl instCompl	—	—
notMem_diff_of_mem 📖	mathematical	Set instMembership	instSDiff	—	—
notMem_of_mem_compl 📖	—	Set instMembership Compl.compl instCompl	—	—	—
notMem_of_mem_diff 📖	—	Set instMembership instSDiff	—	—	—
pair_diff_left 📖	mathematical	—	Set instSDiff instInsert instSingletonSet	—	insert_diff_of_mem mem_singleton diff_singleton_eq_self
pair_diff_right 📖	mathematical	—	Set instSDiff instInsert instSingletonSet	—	pair_comm pair_diff_left
sdiff_inter_right_comm 📖	mathematical	—	Set instInter instSDiff	—	sdiff_inf_right_comm
sdiff_sep_self 📖	mathematical	—	Set instSDiff setOf instMembership	—	diff_self_inter
ssubset_iff_sdiff_singleton 📖	mathematical	—	Set instHasSSubset instMembership instHasSubset instSDiff instSingletonSet	—	—
subset_compl_comm 📖	mathematical	—	Set instHasSubset Compl.compl instCompl	—	le_compl_iff_le_compl
subset_compl_iff_disjoint_left 📖	mathematical	—	Set instHasSubset Compl.compl instCompl Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	—	le_compl_iff_disjoint_left
subset_compl_iff_disjoint_right 📖	mathematical	—	Set instHasSubset Compl.compl instCompl Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	—	le_compl_iff_disjoint_right
subset_compl_singleton_iff 📖	mathematical	—	Set instHasSubset Compl.compl instCompl instSingletonSet instMembership	—	subset_compl_comm singleton_subset_iff
subset_diff 📖	mathematical	—	Set instHasSubset instSDiff Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	—	le_iff_subset le_sdiff
subset_diff_singleton 📖	mathematical	Set instHasSubset instMembership	instSDiff instSingletonSet	—	subset_inter subset_compl_comm singleton_subset_iff
subset_diff_union 📖	mathematical	—	Set instHasSubset instUnion instSDiff	—	le_sdiff_sup
subset_insert_diff_singleton 📖	mathematical	—	Set instHasSubset instInsert instSDiff instSingletonSet	—	diff_singleton_subset_iff subset_refl instReflSubset
subset_insert_iff 📖	mathematical	—	Set instHasSubset instInsert instMembership instSDiff instSingletonSet	—	—
subset_inter_union_compl_left 📖	mathematical	—	Set instHasSubset instUnion instInter Compl.compl instCompl	—	inter_union_distrib_right union_compl_self univ_inter
subset_inter_union_compl_right 📖	mathematical	—	Set instHasSubset instUnion instInter Compl.compl instCompl	—	inter_union_distrib_right union_compl_self inter_univ
subset_ite 📖	mathematical	—	Set instHasSubset ite instInter instSDiff	—	instIsEmptyFalse
subset_union_compl_iff_inter_subset 📖	mathematical	—	Set instHasSubset instUnion Compl.compl instCompl instInter	—	IsCompl.le_sup_right_iff_inf_left_le isCompl_compl
union_compl_self 📖	mathematical	—	Set instUnion Compl.compl instCompl univ	—	eq_univ_iff_forall em
union_diff_cancel 📖	mathematical	Set instHasSubset	instUnion instSDiff	—	sup_sdiff_cancel_right
union_diff_cancel' 📖	mathematical	Set instHasSubset	instUnion instSDiff	—	sup_sdiff_cancel'
union_diff_cancel_left 📖	mathematical	Set instHasSubset instInter instEmptyCollection	instSDiff instUnion	—	Disjoint.sup_sdiff_cancel_left disjoint_iff_inf_le
union_diff_cancel_right 📖	mathematical	Set instHasSubset instInter instEmptyCollection	instSDiff instUnion	—	Disjoint.sup_sdiff_cancel_right disjoint_iff_inf_le
union_diff_distrib 📖	mathematical	—	Set instSDiff instUnion	—	sup_sdiff
union_diff_left 📖	mathematical	—	Set instSDiff instUnion	—	sup_sdiff_left_self
union_diff_right 📖	mathematical	—	Set instSDiff instUnion	—	sup_sdiff_right_self
union_diff_self 📖	mathematical	—	Set instUnion instSDiff	—	sup_sdiff_self
union_eq_compl_compl_inter_compl 📖	mathematical	—	Set instUnion Compl.compl instCompl instInter	—	ext or_iff_not_and_not
union_eq_diff_union_diff_union_inter 📖	mathematical	—	Set instUnion instSDiff instInter	—	sup_eq_sdiff_sup_sdiff_sup_inf
union_inter_compl_left_subset 📖	mathematical	—	Set instHasSubset instInter instUnion Compl.compl instCompl	—	union_inter_distrib_right inter_compl_self empty_union
union_inter_compl_right_subset 📖	mathematical	—	Set instHasSubset instInter instUnion Compl.compl instCompl	—	union_inter_distrib_right inter_compl_self union_empty

---

← Back to Index