Skip to content

Commit

Permalink
chore(data/set/lattice): fix name (#9520)
Browse files Browse the repository at this point in the history
`comp` is for composition, `compl` for complement. Fix names using `comp` instead of `compl`.
  • Loading branch information
sgouezel committed Oct 3, 2021
1 parent 465508f commit 52495a0
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/data/set/lattice.lean
Expand Up @@ -237,11 +237,11 @@ compl_supr
compl_infi

-- classical -- complete_boolean_algebra
theorem Union_eq_comp_Inter_comp (s : ι → set β) : (⋃ i, s i) = (⋂ i, (s i)ᶜ)ᶜ :=
theorem Union_eq_compl_Inter_compl (s : ι → set β) : (⋃ i, s i) = (⋂ i, (s i)ᶜ)ᶜ :=
by simp only [compl_Inter, compl_compl]

-- classical -- complete_boolean_algebra
theorem Inter_eq_comp_Union_comp (s : ι → set β) : (⋂ i, s i) = (⋃ i, (s i)ᶜ)ᶜ :=
theorem Inter_eq_compl_Union_compl (s : ι → set β) : (⋂ i, s i) = (⋃ i, (s i)ᶜ)ᶜ :=
by simp only [compl_Union, compl_compl]

theorem inter_Union (s : set β) (t : ι → set β) :
Expand Down Expand Up @@ -786,7 +786,7 @@ theorem compl_sInter (S : set (set α)) :
by rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

-- classical
theorem sInter_eq_comp_sUnion_compl (S : set (set α)) :
theorem sInter_eq_compl_sUnion_compl (S : set (set α)) :
⋂₀ S = (⋃₀ (compl '' S))ᶜ :=
by rw [←compl_compl (⋂₀ S), compl_sInter]

Expand Down

0 comments on commit 52495a0

Please sign in to comment.