α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ {b | f b ≤ g b} ∩ closure ({b | f b ≤ g b}ᶜ) ⊆ {b | f b = g b}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ frontier {b | f b ≤ g b} ⊆ {b | f b = g b}
rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ b ∈ {b | f b = g b}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ {b | f b ≤ g b} ∩ closure ({b | f b ≤ g b}ᶜ) ⊆ {b | f b = g b}
rintro b ⟨hb₁, hb₂⟩
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ b ∈ closure {b | g b < f b}
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ b ∈ {b | f b = g b}
refine' le_antisymm hb₁ (closure_lt_subset_le hg hf _)
case h.e'_5.h.e'_3
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ b ∈ closure {b | g b < f b}
convert hb₂ using 2
case h.e'_5.h.e'_3
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ
case h.e'_5.h.e'_3
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ
simp only [not_le.symm]
no goals
case h.e'_5.h.e'_3
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure ({b | f b ≤ g b}ᶜ)
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ
rfl