Theorem: ContinuousOn.isClosed_le (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed {x | x ∈ s ∧ f x ≤ g x}
Tactic:
rw [Set.setOf_and]
State after:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed ({a | a ∈ s} ∩ {a | f a ≤ g a})

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed ({a | a ∈ s} ∩ {a | f a ≤ g a})
Tactic:
simp only [Set.setOf_mem_eq]
State after:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed (s ∩ {a | f a ≤ g a})

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
set t := {p : B × B | p.fst ≤ p.snd}
State after:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
⊢ IsClosed (s ∩ {a | f a ≤ g a})

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
set fg := fun x ↦ (f x, g x)
State after:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ IsClosed (s ∩ {a | f a ≤ g a})

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
have e : {x | f x ≤ g x} = fg ⁻¹' t := by
  apply Set.ext; intro x; simp only [Set.preimage_setOf_eq, t]
State after:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ {a | f a ≤ g a})

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
rw [e]
State after:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ fg ⁻¹' t)

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ fg ⁻¹' t)
Tactic:
exact ContinuousOn.preimage_isClosed_of_isClosed (ContinuousOn.prod fc gc) sc
  OrderClosedTopology.isClosed_le'
State after:
no goals

State before:
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ {x | f x ≤ g x} = fg ⁻¹' t
Tactic:
apply Set.ext
State after:
case h
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ ∀ (x : A), x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t

State before:
case h
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ ∀ (x : A), x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t
Tactic:
intro x
State after:
case h
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
x : A
⊢ x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t

State before:
case h
E : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
x : A
⊢ x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t
Tactic:
simp only [Set.preimage_setOf_eq, t]
State after:
no goals