[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen s
⊢ ∀ (t : Set α), t ∈ {s} → IsOpen t
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
I : Set ι
hI : Set.Countable I
f : ι → Set α
hf : ∀ (i : ι), i ∈ I → IsOpen (f i)
⊢ ∀ (t : Set α), t ∈ f '' I → IsOpen t
[PROOFSTEP]
rwa [ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
I : Set ι
hI : Set.Countable I
f : ι → Set α
hf : ∀ (i : ι), i ∈ I → IsOpen (f i)
⊢ ⋂ (i : ι) (_ : i ∈ I), f i = ⋂₀ (f '' I)
[PROOFSTEP]
rw [sInter_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ ∀ (t : Set α), t ∈ range f → IsOpen t
[PROOFSTEP]
rwa [forall_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ ⋂ (i : ι), f i = ⋂₀ range f
[PROOFSTEP]
rw [sInter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
hs : ∀ (i : ι), IsGδ (s i)
⊢ IsGδ (⋂ (i : ι), s i)
[PROOFSTEP]
choose T hTo hTc hTs using hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), s i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), s i)
[PROOFSTEP]
obtain rfl : s = fun i => ⋂₀ T i := funext hTs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), (fun i => ⋂₀ T i) i)
[PROOFSTEP]
refine' ⟨⋃ i, T i, _, countable_iUnion hTc, (sInter_iUnion _).symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ (t : Set α), t ∈ ⋃ (i : ι), T i → IsOpen t
[PROOFSTEP]
simpa [@forall_swap ι] using hTo
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (i : ι) (h : i ∈ s), t i h)
[PROOFSTEP]
rw [biInter_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
haveI := hs.toEncodable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Encodable ↑s
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
exact isGδ_iInter fun x => ht x x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
h : ∀ (s : Set α), s ∈ S → IsGδ s
hS : Set.Countable S
⊢ IsGδ (⋂₀ S)
[PROOFSTEP]
simpa only [sInter_eq_biInter] using isGδ_biInter hS h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)
[PROOFSTEP]
rw [inter_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ (b : Bool), bif b then s else t)
[PROOFSTEP]
exact isGδ_iInter (Bool.forall_bool.2 ⟨ht, hs⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∪ t)
[PROOFSTEP]
rcases hs with ⟨S, Sopen, Scount, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
t : Set α
ht : IsGδ t
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
⊢ IsGδ (⋂₀ S ∪ t)
[PROOFSTEP]
rcases ht with ⟨T, Topen, Tcount, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
⊢ IsGδ (⋂₀ S ∪ ⋂₀ T)
[PROOFSTEP]
rw [sInter_union_sInter]
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
⊢ IsGδ (⋂ (p : Set α × Set α) (_ : p ∈ S ×ˢ T), p.fst ∪ p.snd)
[PROOFSTEP]
apply isGδ_biInter_of_open (Scount.prod Tcount)
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
⊢ ∀ (i : Set α × Set α), i ∈ S ×ˢ T → IsOpen (i.fst ∪ i.snd)
[PROOFSTEP]
rintro ⟨a, b⟩ ⟨ha, hb⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
a b : Set α
ha : (a, b).fst ∈ S
hb : (a, b).snd ∈ T
⊢ IsOpen ((a, b).fst ∪ (a, b).snd)
[PROOFSTEP]
exact (Sopen a ha).union (Topen b hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
refine' Finite.induction_on hs (by simp) _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ (∀ (i : ι), i ∈ ∅ → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ ∅), f i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (∀ (i : ι), i ∈ insert a s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ insert a s), f i)
[PROOFSTEP]
simp only [ball_insert_iff, biUnion_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (IsGδ (f a) ∧ ∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (f a ∪ ⋃ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
exact fun _ _ ihs H => H.1.union (ihs H.2)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
⊢ IsGδ s
[PROOFSTEP]
rcases(@uniformity_hasBasis_open α _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
[GOAL]
case intro.intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ s
[PROOFSTEP]
rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
[GOAL]
case intro.intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ) (_ : True), ⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U i)))
[PROOFSTEP]
refine' isGδ_biInter (to_countable _) fun n _ => IsOpen.isGδ _
[GOAL]
case intro.intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
n : ℕ
x✝ : n ∈ fun i => True
⊢ IsOpen (⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U n)))
[PROOFSTEP]
exact isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ sᶜ
[PROOFSTEP]
rw [← biUnion_of_singleton s, compl_iUnion₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ (⋂ (i : α) (_ : i ∈ s), {i}ᶜ)
[PROOFSTEP]
exact isGδ_biInter hs fun x _ => isGδ_compl_singleton x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
⊢ IsGδ {a}
[PROOFSTEP]
rcases(nhds_basis_opens a).exists_antitone_subbasis with ⟨U, hU, h_basis⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ {a}
[PROOFSTEP]
rw [← biInter_basis_nhds h_basis.toHasBasis]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ (⋂ (i : ℕ) (_ : True), U i)
[PROOFSTEP]
exact isGδ_biInter (to_countable _) fun n _ => (hU n).2.isGδ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
⊢ IsGδ {x | ContinuousAt f x}
[PROOFSTEP]
obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric β _).exists_antitone_subbasis
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | ContinuousAt f x}
[PROOFSTEP]
simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | Tendsto (fun x => (f x.fst, f x.snd)) (𝓝 x ×ˢ 𝓝 x) (uniformity β)}
[PROOFSTEP]
simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis, forall_prop_of_true, setOf_forall, id]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ), {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U i})
[PROOFSTEP]
refine' isGδ_iInter fun k => IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
⊢ x ∈ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} →
    {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
[PROOFSTEP]
rintro ⟨s, ⟨hsx, hso⟩, hsU⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
s : Set α
hsU : ∀ (x : α × α), x ∈ s ×ˢ s → (f x.fst, f x.snd) ∈ U k
hsx : x ∈ s
hso : IsOpen s
⊢ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
⊢ CountableInterFilter (residual α)
[PROOFSTEP]
rw [residual]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
⊢ CountableInterFilter (countableGenerate {t | IsOpen t ∧ Dense t})
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set α
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual α
[PROOFSTEP]
rcases ho with ⟨T, To, Tct, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
T : Set (Set α)
To : ∀ (t : Set α), t ∈ T → IsOpen t
Tct : Set.Countable T
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual α
[PROOFSTEP]
exact (countable_sInter_mem Tct).mpr fun t tT => residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ (∃ S, S ⊆ {t | IsOpen t ∧ Dense t} ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
[PROOFSTEP]
simp_rw [subset_def, mem_setOf, forall_and, and_assoc]


[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ find c ne i ∈ c
[PROOFSTEP]
rw [find]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ (if hi : ∃ v, v ∈ c ∧ i ∈ v.carrier then Exists.choose hi else Set.Nonempty.some ne) ∈ c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ Exists.choose h ∈ c
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ¬∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ Set.Nonempty.some ne ∈ c
[PROOFSTEP]
exacts [h.choose_spec.1, ne.some_mem]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ i ∈ (find c ne i).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
rw [find]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ i ∈ (if hi : ∃ v, v ∈ c ∧ i ∈ v.carrier then Exists.choose hi else Set.Nonempty.some ne).carrier ↔
    i ∈ chainSupCarrier c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
have := h.choose_spec
[GOAL]
case pos
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∃ v, v ∈ c ∧ i ∈ v.carrier
this : Exists.choose h ∈ c ∧ i ∈ (Exists.choose h).carrier
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)
[GOAL]
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ¬∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∀ (v : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
refine iff_of_false (h _ ne.some_mem) ?_
[GOAL]
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∀ (v : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ ¬i ∈ chainSupCarrier c
[PROOFSTEP]
simpa only [chainSupCarrier, mem_iUnion₂, not_exists]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
rcases em (∃ i, i ∉ chainSupCarrier c ∧ x ∈ u i) with (⟨i, hi, hxi⟩ | hx)
[GOAL]
case inl.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
i : ι
hi : ¬i ∈ chainSupCarrier c
hxi : x ∈ u i
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
use i
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
i : ι
hi : ¬i ∈ chainSupCarrier c
hxi : x ∈ u i
⊢ x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
simpa only [(find c ne i).apply_eq (mt (mem_find_carrier_iff _).1 hi)]
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ¬∃ i, ¬i ∈ chainSupCarrier c ∧ x ∈ u i
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
simp_rw [not_exists, not_and, not_imp_not, chainSupCarrier, mem_iUnion₂] at hx
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ i j, x_1 ∈ i.carrier
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
haveI : Nonempty (PartialRefinement u s) := ⟨ne.some⟩
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ i j, x_1 ∈ i.carrier
this : Nonempty (PartialRefinement u s)
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
choose! v hvc hiv using hx
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
rcases(hfin x hxs).exists_maximal_wrt v _ (mem_iUnion.1 (hU hxs)) with
  ⟨i, hxi : x ∈ u i, hmax : ∀ j, x ∈ u j → v i ≤ v j → v i = v j⟩
[GOAL]
case inr.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
rcases mem_iUnion.1 ((v i).subset_iUnion hxs) with ⟨j, hj⟩
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
⊢ x ∈ (fun i => toFun (find c ne i) i) j
[PROOFSTEP]
have hj' : x ∈ u j := (v i).subset _ hj
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
hj' : x ∈ u j
⊢ x ∈ (fun i => toFun (find c ne i) i) j
[PROOFSTEP]
have : v j ≤ v i := (hc.total (hvc _ hxi) (hvc _ hj')).elim (fun h => (hmax j hj' h).ge) id
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this✝ : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
hj' : x ∈ u j
this : v j ≤ v i
⊢ x ∈ (fun i => toFun (find c ne i) i) j
[PROOFSTEP]
simpa only [find_apply_of_mem hc ne (hvc _ hxi) (this.1 <| hiv _ hj')]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∃ v', v < v'
[PROOFSTEP]
have I : (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) ⊆ v i :=
  by
  simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
  intro x hxs H
  rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
  exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
⊢ s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
[PROOFSTEP]
simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∀ (x : X), x ∈ s → (∀ (i_1 : ι), i_1 ≠ i → x ∈ (toFun v i_1)ᶜ) → x ∈ toFun v i
[PROOFSTEP]
intro x hxs H
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
x : X
hxs : x ∈ s
H : ∀ (i_1 : ι), i_1 ≠ i → x ∈ (toFun v i_1)ᶜ
⊢ x ∈ toFun v i
[PROOFSTEP]
rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
[GOAL]
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
x : X
hxs : x ∈ s
H : ∀ (i_1 : ι), i_1 ≠ i → x ∈ (toFun v i_1)ᶜ
j : ι
hj : x ∈ toFun v j
⊢ x ∈ toFun v i
[PROOFSTEP]
exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
⊢ ∃ v', v < v'
[PROOFSTEP]
have C : IsClosed (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) :=
  IsClosed.inter hs (isClosed_biInter fun _ _ => isClosed_compl_iff.2 <| v.isOpen _)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
⊢ ∃ v', v < v'
[PROOFSTEP]
rcases normal_exists_closure_subset C (v.isOpen i) I with ⟨vi, ovi, hvi, cvi⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∃ v', v < v'
[PROOFSTEP]
refine' ⟨⟨update v i vi, insert i v.carrier, _, _, _, _⟩, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∀ (i_1 : ι), IsOpen (update v.toFun i vi i_1)
[PROOFSTEP]
intro j
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
⊢ IsOpen (update v.toFun i vi j)
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hne)
[GOAL]
case intro.intro.intro.refine'_1.inl
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
vi : Set X
ovi : IsOpen vi
j : ι
hi : ¬j ∈ v.carrier
I : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ toFun v j
C : IsClosed (s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ)
hvi : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v j
⊢ IsOpen (update v.toFun j vi j)
[PROOFSTEP]
simp [*, v.isOpen]
[GOAL]
case intro.intro.intro.refine'_1.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hne : j ≠ i
⊢ IsOpen (update v.toFun i vi j)
[PROOFSTEP]
simp [*, v.isOpen]
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ s ⊆ ⋃ (i_1 : ι), update v.toFun i vi i_1
[PROOFSTEP]
refine' fun x hx => mem_iUnion.2 _
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
rcases em (∃ (j : _) (_ : j ≠ i), x ∈ v j) with (⟨j, hji, hj⟩ | h)
[GOAL]
case intro.intro.intro.refine'_2.inl.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ toFun v j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ toFun v j
⊢ x ∈ update v.toFun i vi j
[PROOFSTEP]
rwa [update_noteq hji]
[GOAL]
case intro.intro.intro.refine'_2.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ¬∃ j x_1, x ∈ toFun v j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
push_neg at h
[GOAL]
case intro.intro.intro.refine'_2.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → ¬x ∈ toFun v j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
use i
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → ¬x ∈ toFun v j
⊢ x ∈ update v.toFun i vi i
[PROOFSTEP]
rw [update_same]
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → ¬x ∈ toFun v j
⊢ x ∈ vi
[PROOFSTEP]
exact hvi ⟨hx, mem_biInter h⟩
[GOAL]
case intro.intro.intro.refine'_3
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → closure (update v.toFun i vi i_1) ⊆ u i_1
[PROOFSTEP]
rintro j (rfl | hj)
[GOAL]
case intro.intro.intro.refine'_3.inl
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
vi : Set X
ovi : IsOpen vi
j : ι
hi : ¬j ∈ v.carrier
I : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ toFun v j
C : IsClosed (s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ)
hvi : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v j
⊢ closure (update v.toFun j vi j) ⊆ u j
[PROOFSTEP]
rwa [update_same, ← v.apply_eq hi]
[GOAL]
case intro.intro.intro.refine'_3.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : j ∈ v.carrier
⊢ closure (update v.toFun i vi j) ⊆ u j
[PROOFSTEP]
rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
[GOAL]
case intro.intro.intro.refine'_3.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : j ∈ v.carrier
⊢ closure (toFun v j) ⊆ u j
[PROOFSTEP]
exact v.closure_subset hj
[GOAL]
case intro.intro.intro.refine'_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∀ {i_1 : ι}, ¬i_1 ∈ insert i v.carrier → update v.toFun i vi i_1 = u i_1
[PROOFSTEP]
intro j hj
[GOAL]
case intro.intro.intro.refine'_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : ¬j ∈ insert i v.carrier
⊢ update v.toFun i vi j = u j
[PROOFSTEP]
rw [mem_insert_iff, not_or] at hj
[GOAL]
case intro.intro.intro.refine'_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : ¬j = i ∧ ¬j ∈ v.carrier
⊢ update v.toFun i vi j = u j
[PROOFSTEP]
rw [update_noteq hj.1, v.apply_eq hj.2]
[GOAL]
case intro.intro.intro.refine'_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ v.carrier ⊆
      { toFun := update v.toFun i vi, carrier := insert i v.carrier,
          isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
          subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_1 : ι), update v.toFun i vi i_1),
          closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
          apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }.carrier ∧
    ∀ (i_1 : ι),
      i_1 ∈ v.carrier →
        toFun v i_1 =
          toFun
            { toFun := update v.toFun i vi, carrier := insert i v.carrier,
              isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
              subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_2 : ι), update v.toFun i vi i_2),
              closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
              apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }
            i_1
[PROOFSTEP]
refine' ⟨subset_insert _ _, fun j hj => _⟩
[GOAL]
case intro.intro.intro.refine'_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : j ∈ v.carrier
⊢ toFun v j =
    toFun
      { toFun := update v.toFun i vi, carrier := insert i v.carrier,
        isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
        subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_1 : ι), update v.toFun i vi i_1),
        closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
        apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }
      j
[PROOFSTEP]
exact (update_noteq (ne_of_mem_of_not_mem hj hi) _ _).symm
[GOAL]
case intro.intro.intro.refine'_6
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ¬({ toFun := update v.toFun i vi, carrier := insert i v.carrier,
            isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
            subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_1 : ι), update v.toFun i vi i_1),
            closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
            apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }.carrier ⊆
        v.carrier ∧
      ∀ (i_1 : ι),
        i_1 ∈
            { toFun := update v.toFun i vi, carrier := insert i v.carrier,
                isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
                subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_2 : ι), update v.toFun i vi i_2),
                closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
                apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }.carrier →
          toFun
              { toFun := update v.toFun i vi, carrier := insert i v.carrier,
                isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
                subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_2 : ι), update v.toFun i vi i_2),
                closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
                apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }
              i_1 =
            toFun v i_1)
[PROOFSTEP]
exact fun hle => hi (hle.1 <| mem_insert _ _)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
haveI : Nonempty (PartialRefinement u s) := ⟨⟨u, ∅, uo, us, False.elim, fun _ => rfl⟩⟩
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this : Nonempty (PartialRefinement u s)
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
have : ∀ c : Set (PartialRefinement u s), IsChain (· ≤ ·) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub := fun c hc ne =>
  ⟨.chainSup c hc ne uf us, fun v hv => PartialRefinement.le_chainSup _ _ _ _ hv⟩
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
rcases zorn_nonempty_partialOrder this with ⟨v, hv⟩
[GOAL]
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
suffices : ∀ i, i ∈ v.carrier
[GOAL]
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝¹ : Nonempty (PartialRefinement u s)
this✝ :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
case this
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
[PROOFSTEP]
exact ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩
[GOAL]
case this
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
[PROOFSTEP]
contrapose! hv
[GOAL]
case this
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∃ i, ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
[PROOFSTEP]
rcases hv with ⟨i, hi⟩
[GOAL]
case this.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
[PROOFSTEP]
rcases v.exists_gt hs i hi with ⟨v', hlt⟩
[GOAL]
case this.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
v' : PartialRefinement u s
hlt : v < v'
⊢ ∃ a, v ≤ a ∧ a ≠ v
[PROOFSTEP]
exact ⟨v', hlt.le, hlt.ne'⟩


[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ Matrix.det ↑A * Matrix.det ↑A⁻¹ = 1
[PROOFSTEP]
rw [← det_mul, A.mul_inv, det_one]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ Matrix.det ↑A⁻¹ * Matrix.det ↑A = 1
[PROOFSTEP]
rw [← det_mul, A.inv_mul, det_one]
[GOAL]
n : Type u
R : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrderedCommRing R
inst✝ : Fact (Even (Fintype.card n))
g : { x // x ∈ GLPos n R }
⊢ -↑g ∈ GLPos n R
[PROOFSTEP]
rw [mem_glpos, GeneralLinearGroup.det_apply_val, Units.val_neg, det_neg,
  (Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]
[GOAL]
n : Type u
R : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrderedCommRing R
inst✝ : Fact (Even (Fintype.card n))
g : { x // x ∈ GLPos n R }
⊢ 0 < det ↑↑g
[PROOFSTEP]
exact g.prop
[GOAL]
R : Type ?u.1604470
inst✝ : Field R
a b : R
hab : a ^ 2 + b ^ 2 ≠ 0
⊢ det (↑of ![![a, -b], ![b, a]]) ≠ 0
[PROOFSTEP]
simpa [det_fin_two, sq] using hab


[GOAL]
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
x : E
I : Type u_3
inst✝ : TopologicalSpace I
h✝ : IsEvenlyCovered f (f x) I
e : Trivialization I f := Classical.choose (_ : ∃ t, f x ∈ t.baseSet)
h : f x ∈ (Classical.choose (_ : ∃ t, f x ∈ t.baseSet)).baseSet := Classical.choose_spec h✝.right
he : (f x, (↑e x).snd) = ↑e x := Trivialization.mk_proj_snd' e h
⊢ (f x, (↑e x).snd) ∈ e.target
[PROOFSTEP]
rwa [he, e.mem_target, e.coe_fst (e.mem_source.mpr h)]
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
⊢ IsLocallyHomeomorphOn f (f ⁻¹' s)
[PROOFSTEP]
refine' IsLocallyHomeomorphOn.mk f (f ⁻¹' s) fun x hx => _
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
let e := (hf (f x) hx).toTrivialization
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
have h := (hf (f x) hx).mem_toTrivialization_baseSet
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
h : f x ∈ (IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))).baseSet
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
let he := e.mem_source.2 h
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
h : f x ∈ (IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))).baseSet
he : x ∈ e.source := Iff.mpr (Trivialization.mem_source e) h
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
refine'
  ⟨e.toLocalHomeomorph.trans
      { toFun := fun p => p.1
        invFun := fun p => ⟨p, x, rfl⟩
        source := e.baseSet ×ˢ ({⟨x, rfl⟩} : Set (f ⁻¹' {f x}))
        target := e.baseSet
        open_source := e.open_baseSet.prod (singletons_open_iff_discrete.2 (hf (f x) hx).1 ⟨x, rfl⟩)
        open_target := e.open_baseSet
        map_source' := fun p => And.left
        map_target' := fun p hp => ⟨hp, rfl⟩
        left_inv' := fun p hp => Prod.ext rfl hp.2.symm
        right_inv' := fun p _ => rfl
        continuous_toFun := continuous_fst.continuousOn
        continuous_invFun := (continuous_id'.prod_mk continuous_const).continuousOn },
    ⟨he, by rwa [e.toLocalHomeomorph.symm_symm, e.proj_toFun x he], (hf (f x) hx).toTrivialization_apply⟩, fun p h =>
    (e.proj_toFun p h.1).symm⟩
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
h : f x ∈ (IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))).baseSet
he : x ∈ e.source := Iff.mpr (Trivialization.mem_source e) h
⊢ (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e.toLocalHomeomorph)) x).fst ∈ e.baseSet
[PROOFSTEP]
rwa [e.toLocalHomeomorph.symm_symm, e.proj_toFun x he]
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
⊢ IsCoveringMap f ↔ IsCoveringMapOn f Set.univ
[PROOFSTEP]
simp only [IsCoveringMap, IsCoveringMapOn, Set.mem_univ, forall_true_left]


[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f✝ f g : PartitionOfUnity ι X s
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f g : PartitionOfUnity ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ (x : X), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), ↑(toFun✝ i) x ≤ 1
h : (mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝).toFun = g.toFun
⊢ mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i => support ↑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
sum_eq_one'✝¹ : ∀ (x : X), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝¹ i) x = 1
sum_le_one'✝¹ : ∀ (x : X), ∑ᶠ (i : ι), ↑(toFun✝¹ i) x ≤ 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ (x : X), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), ↑(toFun✝ i) x ≤ 1
h :
  (mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ sum_eq_one'✝¹ sum_le_one'✝¹).toFun =
    (mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝).toFun
⊢ mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ sum_eq_one'✝¹ sum_le_one'✝¹ =
    mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ ∃ i, 0 < ↑(↑f i) x
[PROOFSTEP]
have H := f.sum_eq_one hx
[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∑ᶠ (i : ι), ↑(↑f i) x = 1
⊢ ∃ i, 0 < ↑(↑f i) x
[PROOFSTEP]
contrapose! H
[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), ↑(↑f i) x ≤ 0
⊢ ∑ᶠ (i : ι), ↑(↑f i) x ≠ 1
[PROOFSTEP]
simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f✝ f g : BumpCovering ι X s
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f g : BumpCovering ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ (x : X), x ∈ s → ∃ i, ↑(toFun✝ i) =ᶠ[𝓝 x] 1
h : (mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝).toFun = g.toFun
⊢ mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i => support ↑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
le_one'✝¹ : toFun✝¹ ≤ 1
eventuallyEq_one'✝¹ : ∀ (x : X), x ∈ s → ∃ i, ↑(toFun✝¹ i) =ᶠ[𝓝 x] 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ (x : X), x ∈ s → ∃ i, ↑(toFun✝ i) =ᶠ[𝓝 x] 1
h :
  (mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ le_one'✝¹ eventuallyEq_one'✝¹).toFun =
    (mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝).toFun
⊢ mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ le_one'✝¹ eventuallyEq_one'✝¹ =
    mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i_1 | Set.Nonempty ((fun i_2 => support ↑(Pi.single i 1 i_2)) i_1 ∩ t)}
[PROOFSTEP]
refine' ⟨univ, univ_mem, (finite_singleton i).subset _⟩
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
⊢ {i_1 | Set.Nonempty ((fun i_2 => support ↑(Pi.single i 1 i_2)) i_1 ∩ univ)} ⊆ {i}
[PROOFSTEP]
rintro j ⟨x, hx, -⟩
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x✝ : X
j : ι
x : X
hx : x ∈ (fun i_1 => support ↑(Pi.single i 1 i_1)) j
⊢ j ∈ {i}
[PROOFSTEP]
contrapose! hx
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x✝ : X
j : ι
x : X
hx : ¬j ∈ {i}
⊢ ¬x ∈ support ↑(Pi.single i 1 j)
[PROOFSTEP]
rw [mem_singleton_iff] at hx
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x✝ : X
j : ι
x : X
hx : ¬j = i
⊢ ¬x ∈ support ↑(Pi.single i 1 j)
[PROOFSTEP]
simp [hx]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
x✝ : x ∈ s
⊢ ↑(Pi.single i 1 i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
rw [Pi.single_eq_same, ContinuousMap.coe_one]
[GOAL]
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases exists_subset_iUnion_closure_subset hs ho (fun x _ => hf.point_finite x) hU with ⟨V, hsV, hVo, hVU⟩
[GOAL]
case intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
have hVU' : ∀ i, V i ⊆ U i := fun i => Subset.trans subset_closure (hVU i)
[GOAL]
case intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases exists_subset_iUnion_closure_subset hs hVo (fun x _ => (hf.subset hVU').point_finite x) hsV with
  ⟨W, hsW, hWo, hWV⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
choose f hfp hf0 hf1 hf01 using fun i =>
  h01 _ _ (isClosed_compl_iff.2 <| hVo i) isClosed_closure (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
have hsupp : ∀ i, support (f i) ⊆ V i := fun i => support_subset_iff'.2 (hf0 i)
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ↑(f i) ⊆ V i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
refine'
  ⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1, fun i x => (hf01 i x).2, fun x hx =>
      _⟩,
    hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i)⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ↑(f i) ⊆ V i
x : X
hx : x ∈ s
⊢ ∃ i, ↑(f i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ↑(f i) ⊆ V i
x : X
hx : x ∈ s
i : ι
hi : x ∈ W i
⊢ ∃ i, ↑(f i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
exact ⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩
[GOAL]
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases exists_isSubordinate_of_locallyFinite_of_prop p h01 hs V hVo hVf hsV with ⟨f, hfp, hf⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hfp : ∀ (i : ι), p ↑(↑f i)
hf : IsSubordinate f V
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
exact ⟨f, hfp, hf.mono hVU⟩
[GOAL]
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : IsSubordinate f V
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
exact ⟨f, hf.mono hVU⟩
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
h : ↑(↑f i) x = 0
⊢ toPOUFun f i x = 0
[PROOFSTEP]
rw [toPOUFun, h, zero_mul]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
⊢ toPOUFun f i x = ↑(↑f i) x * ∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(↑f j) x)
[PROOFSTEP]
refine' congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => _)
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - ↑(↑f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
[PROOFSTEP]
rw [Ne.def, sub_eq_self] at hj
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(↑f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
[PROOFSTEP]
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(↑f j) x = 0
⊢ WellOrderingRel j i → j ∈ t
[PROOFSTEP]
exact flip (ht j) hj
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
set s := (f.point_finite x).toFinset
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
have hs : (s : Set ι) = {i | f i x ≠ 0} := Finite.coe_toFinset _
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
have A : (support fun i => toPOUFun f i x) ⊆ s := by
  rw [hs]
  exact fun i hi => f.support_toPOUFun_subset i hi
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
⊢ (support fun i => toPOUFun f i x) ⊆ ↑s
[PROOFSTEP]
rw [hs]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
⊢ (support fun i => toPOUFun f i x) ⊆ {i | ↑(↑f i) x ≠ 0}
[PROOFSTEP]
exact fun i hi => f.support_toPOUFun_subset i hi
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
have B : (mulSupport fun i => 1 - f i x) ⊆ s :=
  by
  rw [hs, mulSupport_one_sub]
  exact fun i => id
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
⊢ (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
[PROOFSTEP]
rw [hs, mulSupport_one_sub]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
⊢ (support fun i => ↑(↑f i) x) ⊆ {i | ↑(↑f i) x ≠ 0}
[PROOFSTEP]
exact fun i => id
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B, Finset.prod_one_sub_ordered,
  sub_sub_cancel]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ i in s, toPOUFun f i x = ∑ i in s, ↑(↑f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(↑f j) x)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i _ => _
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝ : i ∈ s
⊢ toPOUFun f i x = ↑(↑f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(↑f j) x)
[PROOFSTEP]
convert f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
[GOAL]
case convert_4
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : WellOrderingRel j i
hj : ↑(↑f j) x ≠ 0
⊢ j ∈ s
[PROOFSTEP]
rwa [Finite.mem_toFinset]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ ∃ t, toPOUFun f i =ᶠ[𝓝 x] ↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑f j))
[PROOFSTEP]
rcases f.locallyFinite x with ⟨U, hU, hf⟩
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
⊢ ∃ t, toPOUFun f i =ᶠ[𝓝 x] ↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑f j))
[PROOFSTEP]
use hf.toFinset
[GOAL]
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
⊢ toPOUFun f i =ᶠ[𝓝 x] ↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - ↑f j))
[PROOFSTEP]
filter_upwards [hU] with y hyU
[GOAL]
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPOUFun f i y = (↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - ↑f j))) y
[PROOFSTEP]
simp only [ContinuousMap.coe_prod, Pi.mul_apply, Finset.prod_apply]
[GOAL]
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPOUFun f i y = ↑(↑f i) y * ∏ c in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), ↑(1 - ↑f c) y
[PROOFSTEP]
apply toPOUFun_eq_mul_prod
[GOAL]
case h.ht
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) y ≠ 0 → j ∈ Finite.toFinset hf
[PROOFSTEP]
intro j _ hj
[GOAL]
case h.ht
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
hj : ↑(↑f j) y ≠ 0
⊢ j ∈ Finite.toFinset hf
[PROOFSTEP]
exact hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ Continuous (toPOUFun f i)
[PROOFSTEP]
refine' (f i).continuous.mul <| continuous_finprod_cond (fun j _ => continuous_const.sub (f j).continuous) _
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - ↑(↑f i) x
[PROOFSTEP]
simp only [mulSupport_one_sub]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => support fun x => ↑(↑f i) x
[PROOFSTEP]
exact f.locallyFinite
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ ∑ᶠ (i : ι), ↑((fun i => ContinuousMap.mk (toPOUFun f i)) i) x = 1
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_eq_self]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ ∏ᶠ (i : ι), (1 - ↑(↑f i) x) = 0
[PROOFSTEP]
apply finprod_eq_zero (fun i => 1 - f i x) (f.ind x hx)
[GOAL]
case hx
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ 1 - ↑(↑f (ind f x hx)) x = 0
[PROOFSTEP]
simp only [f.ind_apply x hx, sub_self]
[GOAL]
case hf
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ Set.Finite (mulSupport fun i => 1 - ↑(↑f i) x)
[PROOFSTEP]
rw [mulSupport_one_sub]
[GOAL]
case hf
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ Set.Finite (support fun i => ↑(↑f i) x)
[PROOFSTEP]
exact f.point_finite x
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ ∑ᶠ (i : ι), ↑((fun i => ContinuousMap.mk (toPOUFun f i)) i) x ≤ 1
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_le_self_iff]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ 0 ≤ ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
exact finprod_nonneg fun i => sub_nonneg.2 <| f.le_one i x


[GOAL]
t : ℝ
⊢ t ∈ I ↔ 1 - t ∈ I
[PROOFSTEP]
rw [mem_Icc, mem_Icc]
[GOAL]
t : ℝ
⊢ 0 ≤ t ∧ t ≤ 1 ↔ 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mp
t : ℝ
⊢ 0 ≤ t ∧ t ≤ 1 → 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
intro
[GOAL]
case mpr
t : ℝ
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1 → 0 ≤ t ∧ t ≤ 1
[PROOFSTEP]
intro
[GOAL]
case mp
t : ℝ
a✝ : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mpr
t : ℝ
a✝ : 0 ≤ 1 - t ∧ 1 - t ≤ 1
⊢ 0 ≤ t ∧ t ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mp.left
t : ℝ
a✝ : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t
[PROOFSTEP]
linarith
[GOAL]
case mp.right
t : ℝ
a✝ : 0 ≤ t ∧ t ≤ 1
⊢ 1 - t ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case mpr.left
t : ℝ
a✝ : 0 ≤ 1 - t ∧ 1 - t ≤ 1
⊢ 0 ≤ t
[PROOFSTEP]
linarith
[GOAL]
case mpr.right
t : ℝ
a✝ : 0 ≤ 1 - t ∧ 1 - t ≤ 1
⊢ t ≤ 1
[PROOFSTEP]
linarith
[GOAL]
⊢ 1 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case right
⊢ 1 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ ↑(σ 0) = ↑1
[PROOFSTEP]
simp [symm]
[GOAL]
⊢ ↑(σ 1) = ↑0
[PROOFSTEP]
simp [symm]
[GOAL]
x : ↑I
⊢ ↑(σ (σ x)) = ↑x
[PROOFSTEP]
simp [symm]
[GOAL]
⊢ CompactSpace ↑I
[PROOFSTEP]
infer_instance
[GOAL]
x : ↑I
⊢ 0 ≤ 1 - ↑x
[PROOFSTEP]
simpa using x.2.2
[GOAL]
x : ↑I
⊢ 1 - ↑x ≤ 1
[PROOFSTEP]
simpa using x.2.1
[GOAL]
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)
[PROOFSTEP]
constructor
[GOAL]
case mp
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I → t ∈ Icc 0 (1 / a)
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mpr
a t : ℝ
ha : 0 < a
⊢ t ∈ Icc 0 (1 / a) → a * t ∈ I
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mp.intro
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ∈ Icc 0 (1 / a)
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ∈ I
[PROOFSTEP]
constructor
[GOAL]
case mp.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t
[PROOFSTEP]
exact nonneg_of_mul_nonneg_right h₁ ha
[GOAL]
case mp.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a
[PROOFSTEP]
rwa [le_div_iff ha, mul_comm]
[GOAL]
case mpr.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t
[PROOFSTEP]
exact mul_nonneg ha.le h₁
[GOAL]
case mpr.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1
[PROOFSTEP]
rwa [le_div_iff ha, mul_comm] at h₂
[GOAL]
t : ℝ
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1
[PROOFSTEP]
constructor
[GOAL]
case mp
t : ℝ
⊢ 2 * t - 1 ∈ I → t ∈ Icc (1 / 2) 1
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mpr
t : ℝ
⊢ t ∈ Icc (1 / 2) 1 → 2 * t - 1 ∈ I
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mp.intro
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ∈ Icc (1 / 2) 1
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case mp.intro.left
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ 1 / 2 ≤ t
[PROOFSTEP]
linarith
[GOAL]
case mp.intro.right
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case mpr.intro.left
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 0 ≤ 2 * t - 1
[PROOFSTEP]
linarith
[GOAL]
case mpr.intro.right
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ≤ 1
[PROOFSTEP]
linarith
[GOAL]
x : ↑unitInterval
⊢ 0 ≤ ↑x
[PROOFSTEP]
unit_interval
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : 0 < a
⊢ ↑(affineHomeomorph a b (_ : a ≠ 0)) '' Icc 0 1 = Icc b (a + b)
[PROOFSTEP]
simp [h]
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
⊢ ↑(Icc a b) ≃ₜ ↑(Icc 0 1)
[PROOFSTEP]
let e := Homeomorph.image (affineHomeomorph (b - a) a (sub_pos.mpr h).ne.symm) (Set.Icc 0 1)
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ ↑(Icc a b) ≃ₜ ↑(Icc 0 1)
[PROOFSTEP]
refine' (e.trans _).symm
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) ≃ₜ ↑(Icc a b)
[PROOFSTEP]
apply Homeomorph.setCongr
[GOAL]
case h
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ ↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1 = Icc a b
[PROOFSTEP]
rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]
[GOAL]
case h
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ Icc a (b - a + a) = Icc a b
[PROOFSTEP]
simp


[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
f : α✝ → β
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated Set.univ ↔ QuasiSeparatedSpace α
[PROOFSTEP]
rw [QuasiSeparatedSpace_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
f : α✝ → β
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated Set.univ ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
[PROOFSTEP]
simp [IsQuasiSeparated]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
⊢ IsQuasiSeparated (f '' s)
[PROOFSTEP]
intro U V hU hU' hU'' hV hV' hV''
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
[PROOFSTEP]
convert (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image h.continuous
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)
[PROOFSTEP]
symm
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
[PROOFSTEP]
rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V ⊆ Set.range f
[PROOFSTEP]
exact (Set.inter_subset_left _ _).trans (hU.trans (Set.image_subset_range _ _))
[GOAL]
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' U ⊆ s
[PROOFSTEP]
intro x hx
[GOAL]
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ x ∈ s
[PROOFSTEP]
rw [← (h.inj.injOn _).mem_image_iff (Set.subset_univ _) trivial]
[GOAL]
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s
[PROOFSTEP]
exact hU hx
[GOAL]
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)
[PROOFSTEP]
rw [h.isCompact_iff_isCompact_image]
[GOAL]
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' U))
[PROOFSTEP]
convert hU''
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U) = U
[PROOFSTEP]
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ⊆ Set.range f
[PROOFSTEP]
exact hU.trans (Set.image_subset_range _ _)
[GOAL]
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s
[PROOFSTEP]
intro x hx
[GOAL]
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ x ∈ s
[PROOFSTEP]
rw [← (h.inj.injOn _).mem_image_iff (Set.subset_univ _) trivial]
[GOAL]
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s
[PROOFSTEP]
exact hV hx
[GOAL]
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)
[PROOFSTEP]
rw [h.isCompact_iff_isCompact_image]
[GOAL]
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' V))
[PROOFSTEP]
convert hV''
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' V) = V
[PROOFSTEP]
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ V ⊆ Set.range f
[PROOFSTEP]
exact hV.trans (Set.image_subset_range _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : OpenEmbedding f
s : Set α
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)
[PROOFSTEP]
refine' ⟨fun hs => hs.image_of_embedding h.toEmbedding, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : OpenEmbedding f
s : Set α
⊢ IsQuasiSeparated (f '' s) → IsQuasiSeparated s
[PROOFSTEP]
intro H U V hU hU' hU'' hV hV' hV''
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : OpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
[PROOFSTEP]
rw [h.toEmbedding.isCompact_iff_isCompact_image, Set.image_inter h.inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : OpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' U ∩ f '' V)
[PROOFSTEP]
exact
  H (f '' U) (f '' V) (Set.image_subset _ hU) (h.isOpenMap _ hU') (hU''.image h.continuous) (Set.image_subset _ hV)
    (h.isOpenMap _ hV') (hV''.image h.continuous)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s
[PROOFSTEP]
rw [← isQuasiSeparated_univ_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated Set.univ
[PROOFSTEP]
convert (hs.openEmbedding_subtype_val.isQuasiSeparated_iff (s := Set.univ)).symm
[GOAL]
case h.e'_1.h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ s = Subtype.val '' Set.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
⊢ IsQuasiSeparated s
[PROOFSTEP]
intro U V hU hU' hU'' hV hV' hV''
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
[PROOFSTEP]
exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''