Commit 2022-12-24 11:23 863ab3eb

View on Github →

feat: port Data.Set.Pairwise (#1175)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Pairwise.lean

added theorem Pairwise.bunionᵢ_injective

added theorem Pairwise.subset_of_bunionᵢ_subset_bunionᵢ

added theorem Set.InjOn.pairwiseDisjoint_image

added theorem Set.InjOn.pairwise_image

added theorem Set.Nonempty.pairwise_eq_iff_exists_eq

added theorem Set.Nonempty.pairwise_iff_exists_forall

added theorem Set.Pairwise.insert_of_not_mem

added theorem Set.Pairwise.insert_of_symmetric

added theorem Set.Pairwise.insert_of_symmetric_of_not_mem

added theorem Set.Pairwise.mono'

added theorem Set.Pairwise.mono

added theorem Set.PairwiseDisjoint.bunionᵢ

added theorem Set.PairwiseDisjoint.elim'

added theorem Set.PairwiseDisjoint.elim

added theorem Set.PairwiseDisjoint.elim_set

added theorem Set.PairwiseDisjoint.eq_of_le

added theorem Set.PairwiseDisjoint.image_of_le

added theorem Set.PairwiseDisjoint.insert_of_not_mem

added theorem Set.PairwiseDisjoint.mono

added theorem Set.PairwiseDisjoint.mono_on

added theorem Set.PairwiseDisjoint.range

added theorem Set.PairwiseDisjoint.subset

added theorem Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ

added theorem Set.PairwiseDisjoint.union

added def Set.PairwiseDisjoint

added theorem Set.bunionᵢ_diff_bunionᵢ_eq

added theorem Set.pairwiseDisjoint_empty

added theorem Set.pairwiseDisjoint_fiber

added theorem Set.pairwiseDisjoint_image_left_iff

added theorem Set.pairwiseDisjoint_image_right_iff

added theorem Set.pairwiseDisjoint_insert

added theorem Set.pairwiseDisjoint_insert_of_not_mem

added theorem Set.pairwiseDisjoint_range_singleton

added theorem Set.pairwiseDisjoint_singleton

added theorem Set.pairwiseDisjoint_union

added theorem Set.pairwiseDisjoint_unionᵢ

added theorem Set.pairwiseDisjoint_unionₛ

added theorem Set.pairwise_bot_iff

added theorem Set.pairwise_empty

added theorem Set.pairwise_eq_iff_exists_eq

added theorem Set.pairwise_iff_exists_forall

added theorem Set.pairwise_iff_of_refl

added theorem Set.pairwise_insert

added theorem Set.pairwise_insert_of_not_mem

added theorem Set.pairwise_insert_of_symmetric

added theorem Set.pairwise_insert_of_symmetric_of_not_mem

added theorem Set.pairwise_pair

added theorem Set.pairwise_pair_of_symmetric

added theorem Set.pairwise_singleton

added theorem Set.pairwise_top

added theorem Set.pairwise_union

added theorem Set.pairwise_union_of_symmetric

added theorem Set.pairwise_unionᵢ

added theorem Set.pairwise_unionₛ

added theorem Set.pairwise_univ

added theorem Symmetric.pairwise_on

added theorem pairwise_disjoint_fiber

added theorem pairwise_disjoint_mono

added theorem pairwise_disjoint_on

added theorem pairwise_disjoint_on_bool

added theorem pairwise_on_bool

added theorem pairwise_subtype_iff_pairwise_set