Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-11 02:38 3c09987c

View on Github →

docs(data/set/lattice): add module docstring (#8250) This also cleans up some whitespace and replaces some assumes with λs

Estimated changes

modified theorem set.Inter_const
modified theorem set.Inter_set_of
modified theorem set.Inter_univ
modified theorem set.Union_const
modified theorem set.Union_empty
modified theorem set.Union_of_singleton
modified theorem set.Union_prop_neg
modified theorem set.Union_prop_pos
modified theorem set.Union_subset_Union2
modified theorem set.Union_subset_Union
modified theorem set.bInter_image
modified theorem set.bInter_range
modified theorem set.bUnion_range
modified theorem set.bind_def
modified theorem set.image_Union
modified theorem set.image_eq_Union
modified theorem set.mem_sUnion
modified theorem set.monotone_preimage
modified theorem set.not_disjoint_iff
modified theorem set.pairwise_disjoint.range
modified theorem set.pi_def
modified theorem set.pi_diff_pi_subset
modified theorem set.range_eq_Union
modified theorem set.sInter_bUnion
modified theorem set.sUnion_bUnion
modified theorem set.sUnion_subset
modified theorem set.sUnion_subset_iff
modified def set.seq
modified theorem set.seq_def
modified theorem set.seq_singleton
modified def set.sigma_to_Union
modified theorem set.subset_sInter
modified theorem set.univ_disjoint
modified theorem set.univ_subtype