We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 7c45de9 commit d966564Copy full SHA for d966564
1 file changed
Mathlib/Topology/Baire/Lemmas.lean
@@ -59,7 +59,7 @@ theorem IsGδ.baireSpace_of_dense {s : Set X} (hG : IsGδ s) (hd : Dense s) : Ba
59
exact ⟨g, hg1, hg2, fun n => (hg3 n).symm⟩
60
have h_inter_dense : Dense (⋂ n, g n ∩ V n) :=
61
BaireSpace.baire_property (fun n ↦ g n ∩ V n) (fun n => (hg1 n).inter (hV.1 n))
62
- (fun n => (hg2 n).inter_of_isOpen_left (Dense.mono (by simp [hV.2, iInter_subset]) hd)
+ (fun n => (hg2 n).inter_of_isOpen_left (hd.mono (by simp [hV.2, iInter_subset]))
63
(hg1 n))
64
have h_inter_eq : ⋂ n, g n ∩ V n = ⋂ n, f n := by
65
ext
0 commit comments