Skip to content

Commit

Permalink
chore(Data/Set/Lattice): Deduplicate namespace Set. from CABA instance (
Browse files Browse the repository at this point in the history
#10263)

Dedup Set.Set.completeBooleanAlgebra to Set.completeBooleanAlgebra
  • Loading branch information
Shamrock-Frost authored and atarnoam committed Feb 9, 2024
1 parent 00abff7 commit 552b115
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Set/Lattice.lean
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,7 @@ theorem mem_iInter₂_of_mem {s : ∀ i, κ i → Set α} {a : α} (h : ∀ i j,
mem_iInter₂.2 h
#align set.mem_Inter₂_of_mem Set.mem_iInter₂_of_mem

instance Set.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Set α) :=
instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Set α) :=
{ instBooleanAlgebraSet with
le_sSup := fun s t t_in a a_in => ⟨t, t_in, a_in⟩
sSup_le := fun s t h a ⟨t', ⟨t'_in, a_in⟩⟩ => h t' t'_in a_in
Expand Down

0 comments on commit 552b115

Please sign in to comment.