α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
have : { p : G × G | p.fst ≤ p.snd } = (fun p : G × G => p.snd - p.fst) ⁻¹' { x : G | 0 ≤ x } :=
  by ext1 p; simp only [sub_nonneg, Set.preimage_setOf_eq]
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed ((fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x})
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
rw [this]
no goals
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed ((fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x})
exact IsClosed.preimage (continuous_snd.sub continuous_fst) h
case h
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.fst ≤ p.snd} ↔ p ∈ (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
ext1 p
no goals
case h
α : Type ?u.122280
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_1
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.fst ≤ p.snd} ↔ p ∈ (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
simp only [sub_nonneg, Set.preimage_setOf_eq]