Commit 2025-03-04 11:47 0ae75631

View on Github →

chore: split long file Mathlib.Data.Set.Basic (#22484)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

Modified Mathlib/Data/Set/Basic.lean

deleted theorem Antitone.inter

deleted theorem Antitone.union

deleted theorem AntitoneOn.inter

deleted theorem AntitoneOn.union

deleted theorem Disjoint.inter_eq

deleted theorem Disjoint.inter_left'

deleted theorem Disjoint.inter_left

deleted theorem Disjoint.inter_right'

deleted theorem Disjoint.inter_right

deleted theorem Disjoint.subset_left_of_subset_union

deleted theorem Disjoint.subset_right_of_subset_union

deleted theorem Disjoint.union_left

deleted theorem Disjoint.union_right

deleted theorem Monotone.inter

deleted theorem Monotone.union

deleted theorem MonotoneOn.inter

deleted theorem MonotoneOn.union

deleted theorem Set.antitoneOn_iff_antitone

deleted theorem Set.antitone_bforall

deleted theorem Set.antitone_setOf

deleted theorem Set.coe_inclusion

deleted theorem Set.disjoint_compl_left_iff_subset

deleted theorem Set.disjoint_compl_right_iff_subset

deleted theorem Set.disjoint_empty

deleted theorem Set.disjoint_iff_forall_ne

deleted theorem Set.disjoint_iff_inter_eq_empty

deleted theorem Set.disjoint_left

deleted theorem Set.disjoint_of_subset

deleted theorem Set.disjoint_of_subset_iff_left_eq_empty

deleted theorem Set.disjoint_of_subset_left

deleted theorem Set.disjoint_of_subset_right

deleted theorem Set.disjoint_or_nonempty_inter

deleted theorem Set.disjoint_right

deleted theorem Set.disjoint_sdiff_inter

deleted theorem Set.disjoint_sdiff_left

deleted theorem Set.disjoint_sdiff_right

deleted theorem Set.disjoint_union_left

deleted theorem Set.disjoint_union_right

deleted theorem Set.disjoint_univ

deleted theorem Set.empty_disjoint

deleted theorem Set.eq_of_inclusion_surjective

deleted theorem Set.inclusion_comp_inclusion

deleted theorem Set.inclusion_eq_id

deleted theorem Set.inclusion_inclusion

deleted theorem Set.inclusion_inj

deleted theorem Set.inclusion_injective

deleted theorem Set.inclusion_le_inclusion

deleted theorem Set.inclusion_lt_inclusion

deleted theorem Set.inclusion_mk

deleted theorem Set.inclusion_right

deleted theorem Set.inclusion_self

deleted theorem Set.monotoneOn_iff_monotone

deleted theorem Set.monotone_setOf

modified theorem Set.nonempty_coe_sort

deleted theorem Set.not_disjoint_iff

deleted theorem Set.not_disjoint_iff_nonempty_inter

deleted theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le

deleted theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt

deleted theorem Set.strictAntiOn_iff_strictAnti

deleted theorem Set.strictMonoOn_iff_strictMono

deleted theorem Set.subset_compl_iff_disjoint_left

deleted theorem Set.subset_compl_iff_disjoint_right

deleted theorem Set.subset_diff

deleted theorem Set.univ_disjoint

deleted theorem Set.val_comp_inclusion

Created Mathlib/Data/Set/Disjoint.lean

added theorem Disjoint.inter_eq

added theorem Disjoint.inter_left'

added theorem Disjoint.inter_left

added theorem Disjoint.inter_right'

added theorem Disjoint.inter_right

added theorem Disjoint.subset_left_of_subset_union

added theorem Disjoint.subset_right_of_subset_union

added theorem Disjoint.union_left

added theorem Disjoint.union_right

added theorem Set.disjoint_compl_left_iff_subset

added theorem Set.disjoint_compl_right_iff_subset

added theorem Set.disjoint_empty

added theorem Set.disjoint_iff_forall_ne

added theorem Set.disjoint_iff_inter_eq_empty

added theorem Set.disjoint_left

added theorem Set.disjoint_of_subset

added theorem Set.disjoint_of_subset_iff_left_eq_empty

added theorem Set.disjoint_of_subset_left

added theorem Set.disjoint_of_subset_right

added theorem Set.disjoint_or_nonempty_inter

added theorem Set.disjoint_right

added theorem Set.disjoint_sdiff_inter

added theorem Set.disjoint_sdiff_left

added theorem Set.disjoint_sdiff_right

added theorem Set.disjoint_union_left

added theorem Set.disjoint_union_right

added theorem Set.disjoint_univ

added theorem Set.empty_disjoint

added theorem Set.not_disjoint_iff

added theorem Set.not_disjoint_iff_nonempty_inter

added theorem Set.subset_compl_iff_disjoint_left

added theorem Set.subset_compl_iff_disjoint_right

added theorem Set.subset_diff

added theorem Set.univ_disjoint

Modified Mathlib/Data/Set/Image.lean

Created Mathlib/Data/Set/Inclusion.lean

added theorem Set.coe_inclusion

added theorem Set.eq_of_inclusion_surjective

added theorem Set.inclusion_comp_inclusion

added theorem Set.inclusion_eq_id

added theorem Set.inclusion_inclusion

added theorem Set.inclusion_inj

added theorem Set.inclusion_injective

added theorem Set.inclusion_le_inclusion

added theorem Set.inclusion_lt_inclusion

added theorem Set.inclusion_mk

added theorem Set.inclusion_right

added theorem Set.inclusion_self

added theorem Set.val_comp_inclusion

Modified Mathlib/Data/Set/Insert.lean

Created Mathlib/Data/Set/Order.lean

added theorem Antitone.inter

added theorem Antitone.union

added theorem AntitoneOn.inter

added theorem AntitoneOn.union

added theorem Monotone.inter

added theorem Monotone.union

added theorem MonotoneOn.inter

added theorem MonotoneOn.union

added theorem Set.antitoneOn_iff_antitone

added theorem Set.antitone_bforall

added theorem Set.antitone_setOf

added theorem Set.monotoneOn_iff_monotone

added theorem Set.monotone_setOf

added theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le

added theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt

added theorem Set.strictAntiOn_iff_strictAnti

added theorem Set.strictMonoOn_iff_strictMono

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

Modified Mathlib/Tactic/TautoSet.lean

Modified scripts/noshake.json