Commit 2022-12-22 16:59 ce30ba60

View on Github →

feat port: Data.Set.Lattice (#1121) Mostly name changes. The proof of subset_bunionᵢ_of_mem needed a bunch of explicit arguments for some reason. I also moved the definition of set.sUnion from Init.Set into this file and changed its name. I also protected the definition of Set.compl

Estimated changes

added theorem Antitone.inter
added theorem Antitone.union
added theorem AntitoneOn.inter
added theorem AntitoneOn.union
added theorem Disjoint.image
added theorem Disjoint.inter_left'
added theorem Disjoint.inter_left
added theorem Disjoint.inter_right'
added theorem Disjoint.inter_right
added theorem Disjoint.ne_of_mem
added theorem Disjoint.of_image
added theorem Disjoint.of_preimage
added theorem Disjoint.preimage
added theorem Disjoint.union_left
added theorem Disjoint.union_right
added theorem Monotone.inter
added theorem Monotone.union
added theorem MonotoneOn.inter
added theorem MonotoneOn.union
added theorem Set.Ici_supᵢ
added theorem Set.Ici_supᵢ₂
added theorem Set.Ici_supₛ
added theorem Set.Iic_infᵢ
added theorem Set.Iic_infᵢ₂
added theorem Set.Iic_infₛ
added theorem Set.InjOn.image_inter
added theorem Set.Sigma.univ
added theorem Set.antitone_bforall
added theorem Set.antitone_setOf
added theorem Set.bijOn_interᵢ
added theorem Set.bijOn_unionᵢ
added theorem Set.binterᵢ_and'
added theorem Set.binterᵢ_and
added theorem Set.binterᵢ_empty
added theorem Set.binterᵢ_image
added theorem Set.binterᵢ_insert
added theorem Set.binterᵢ_inter
added theorem Set.binterᵢ_mono
added theorem Set.binterᵢ_pair
added theorem Set.binterᵢ_range
added theorem Set.binterᵢ_union
added theorem Set.binterᵢ_unionᵢ
added theorem Set.binterᵢ_univ
added theorem Set.bunionᵢ_and'
added theorem Set.bunionᵢ_and
added theorem Set.bunionᵢ_empty
added theorem Set.bunionᵢ_image
added theorem Set.bunionᵢ_insert
added theorem Set.bunionᵢ_mono
added theorem Set.bunionᵢ_pair
added theorem Set.bunionᵢ_range
added theorem Set.bunionᵢ_self
added theorem Set.bunionᵢ_union
added theorem Set.bunionᵢ_unionᵢ
added theorem Set.bunionᵢ_univ
added theorem Set.compl_interᵢ
added theorem Set.compl_interᵢ₂
added theorem Set.compl_interₛ
added theorem Set.compl_unionᵢ
added theorem Set.compl_unionᵢ₂
added theorem Set.compl_unionₛ
added theorem Set.diff_interᵢ
added theorem Set.diff_unionᵢ
added theorem Set.disjoint_diff
added theorem Set.disjoint_empty
added theorem Set.disjoint_image_iff
added theorem Set.disjoint_of_subset
added theorem Set.disjoint_singleton
added theorem Set.disjoint_univ
added theorem Set.empty_disjoint
added theorem Set.image2_eq_seq
added theorem Set.image2_eq_unionᵢ
added theorem Set.image_eq_unionᵢ
added theorem Set.image_interᵢ
added theorem Set.image_interᵢ₂
added theorem Set.image_seq
added theorem Set.image_unionᵢ
added theorem Set.image_unionᵢ₂
added theorem Set.infᵢ_eq_dif
added theorem Set.infᵢ_eq_interᵢ
added theorem Set.infₛ_eq_interₛ
added theorem Set.inter_binterᵢ
added theorem Set.inter_eq_interᵢ
added theorem Set.inter_interᵢ
added theorem Set.inter_unionᵢ
added theorem Set.inter_unionᵢ₂
added def Set.interᵢ
added theorem Set.interᵢ_and
added theorem Set.interᵢ_coe_set
added theorem Set.interᵢ_comm
added theorem Set.interᵢ_congr
added theorem Set.interᵢ_const
added theorem Set.interᵢ_dite
added theorem Set.interᵢ_eq_if
added theorem Set.interᵢ_eq_univ
added theorem Set.interᵢ_exists
added theorem Set.interᵢ_false
added theorem Set.interᵢ_inter
added theorem Set.interᵢ_ite
added theorem Set.interᵢ_mono'
added theorem Set.interᵢ_mono
added theorem Set.interᵢ_of_empty
added theorem Set.interᵢ_option
added theorem Set.interᵢ_or
added theorem Set.interᵢ_plift_up
added theorem Set.interᵢ_setOf
added theorem Set.interᵢ_subset
added theorem Set.interᵢ_subtype
added theorem Set.interᵢ_true
added theorem Set.interᵢ_union
added theorem Set.interᵢ_univ
added theorem Set.interᵢ₂_comm
added theorem Set.interᵢ₂_congr
added theorem Set.interᵢ₂_mono'
added theorem Set.interᵢ₂_mono
added theorem Set.interᵢ₂_subset
added theorem Set.interᵢ₂_union
added def Set.interₛ
added theorem Set.interₛ_empty
added theorem Set.interₛ_eq_univ
added theorem Set.interₛ_image
added theorem Set.interₛ_insert
added theorem Set.interₛ_pair
added theorem Set.interₛ_prod
added theorem Set.interₛ_range
added theorem Set.interₛ_singleton
added theorem Set.interₛ_union
added theorem Set.interₛ_unionᵢ
added def Set.kernImage
added theorem Set.mapsTo_interᵢ
added theorem Set.mapsTo_interᵢ₂
added theorem Set.mapsTo_interₛ
added theorem Set.mapsTo_unionᵢ
added theorem Set.mapsTo_unionᵢ₂
added theorem Set.mapsTo_unionₛ
added theorem Set.mem_binterᵢ
added theorem Set.mem_bunionᵢ
added theorem Set.mem_interᵢ
added theorem Set.mem_interᵢ₂
added theorem Set.mem_interₛ
added theorem Set.mem_seq_iff
added theorem Set.mem_unionᵢ
added theorem Set.mem_unionᵢ₂
added theorem Set.mem_unionₛ
added theorem Set.monotone_image
added theorem Set.monotone_preimage
added theorem Set.monotone_setOf
added theorem Set.nonempty_bunionᵢ
added theorem Set.nonempty_interᵢ
added theorem Set.nonempty_interₛ
added theorem Set.nonempty_unionᵢ
added theorem Set.nonempty_unionₛ
added theorem Set.not_disjoint_iff
added theorem Set.pi_def
added theorem Set.pi_diff_pi_subset
added theorem Set.preimage_eq_empty
added theorem Set.preimage_interᵢ
added theorem Set.preimage_interₛ
added theorem Set.preimage_unionᵢ
added theorem Set.preimage_unionₛ
added theorem Set.prod_eq_seq
added theorem Set.prod_interₛ
added theorem Set.prod_unionᵢ
added theorem Set.prod_unionᵢ₂
added theorem Set.prod_unionₛ
added theorem Set.range_eq_unionᵢ
added def Set.seq
added theorem Set.seq_def
added theorem Set.seq_mono
added theorem Set.seq_seq
added theorem Set.seq_singleton
added theorem Set.seq_subset
added theorem Set.setOf_exists
added theorem Set.setOf_forall
added theorem Set.singleton_seq
added theorem Set.subset_diff
added theorem Set.subset_interᵢ
added theorem Set.subset_interᵢ₂
added theorem Set.subset_interₛ
added theorem Set.subset_unionᵢ
added theorem Set.subset_unionᵢ₂
added theorem Set.supᵢ_eq_unionᵢ
added theorem Set.supₛ_eq_unionₛ
added theorem Set.surjOn_interᵢ
added theorem Set.surjOn_unionᵢ
added theorem Set.surjOn_unionᵢ₂
added theorem Set.surjOn_unionₛ
added theorem Set.union_eq_unionᵢ
added theorem Set.union_interᵢ
added theorem Set.union_interᵢ₂
added theorem Set.union_unionᵢ
added def Set.unionᵢ
added theorem Set.unionᵢ_and
added theorem Set.unionᵢ_coe_set
added theorem Set.unionᵢ_comm
added theorem Set.unionᵢ_congr
added theorem Set.unionᵢ_const
added theorem Set.unionᵢ_diff
added theorem Set.unionᵢ_dite
added theorem Set.unionᵢ_empty
added theorem Set.unionᵢ_eq_dif
added theorem Set.unionᵢ_eq_empty
added theorem Set.unionᵢ_eq_if
added theorem Set.unionᵢ_exists
added theorem Set.unionᵢ_false
added theorem Set.unionᵢ_inter
added theorem Set.unionᵢ_ite
added theorem Set.unionᵢ_mono'
added theorem Set.unionᵢ_mono
added theorem Set.unionᵢ_of_empty
added theorem Set.unionᵢ_option
added theorem Set.unionᵢ_or
added theorem Set.unionᵢ_plift_up
added theorem Set.unionᵢ_prod
added theorem Set.unionᵢ_setOf
added theorem Set.unionᵢ_subset
added theorem Set.unionᵢ_subtype
added theorem Set.unionᵢ_true
added theorem Set.unionᵢ_union
added theorem Set.unionᵢ_univ_pi
added theorem Set.unionᵢ₂_comm
added theorem Set.unionᵢ₂_congr
added theorem Set.unionᵢ₂_inter
added theorem Set.unionᵢ₂_mono'
added theorem Set.unionᵢ₂_mono
added theorem Set.unionᵢ₂_subset
added def Set.unionₛ
added theorem Set.unionₛ_empty
added theorem Set.unionₛ_eq_empty
added theorem Set.unionₛ_image
added theorem Set.unionₛ_insert
added theorem Set.unionₛ_mono
added theorem Set.unionₛ_pair
added theorem Set.unionₛ_range
added theorem Set.unionₛ_singleton
added theorem Set.unionₛ_subset
added theorem Set.unionₛ_union
added theorem Set.unionₛ_unionᵢ
added theorem Set.univ_disjoint
added theorem Set.univ_subtype
added theorem infᵢ_unionᵢ
added theorem infₛ_unionₛ
added theorem supᵢ_unionᵢ
added theorem supₛ_unionₛ
deleted def Set.compl
deleted def Set.sUnion