internlm/Lean-Github huggingface dataset:
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
h₁ : LipschitzOnWith (Kx ↑i) f (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
refine lipschitz_image_null_set_is_null_set (Nat.cast_nonneg d) h₁ h₂
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
Tactic:
calc f '' (s ∩ (K n))
  _ ⊆ f '' (s ∩ (⋃ (i : v), U i)) := by
    apply image_subset
    apply inter_subset_inter_right s hv
  _ = f '' ((⋃ (i : v), s ∩ (U i))) := by rw [inter_iUnion]
  _ = ⋃ (i : v), f '' ( s ∩ (U i)) := image_iUnion
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ f '' (s ∩ K n) ⊆ f '' (s ∩ ⋃ i, U ↑i)
Tactic:
apply image_subset
Proof state after:
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ s ∩ K n ⊆ s ∩ ⋃ i, U ↑i
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ s ∩ K n ⊆ s ∩ ⋃ i, U ↑i
Tactic:
apply inter_subset_inter_right s hv
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ f '' (s ∩ ⋃ i, U ↑i) = f '' ⋃ i, s ∩ U ↑i
Tactic:
rw [inter_iUnion]
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) ≤ 0
Tactic:
calc μH[d] (f '' (s ∩ (K n)))
  _ ≤ μH[d] (⋃ (i : v), f '' (s ∩ (U i))) := measure_mono this
  _ ≤ ∑' (i : v), (μH[d] (f '' (s ∩ (U i))) : ℝ≥0∞) := by apply measure_iUnion_le
  _ = ∑' (_ : v), (0 : ℝ≥0∞) := tsum_congr hnull
  _ = 0 := by simp
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (⋃ i, f '' (s ∩ U ↑i)) ≤ ∑' (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i))
Tactic:
apply measure_iUnion_le
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ∑' (x : { x // x ∈ v }), 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set_open
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
U : Set X
hf : LocallyLipschitz (U.restrict f)
s : Set X
hsu : s ⊆ U
hs : ↑μH[↑d] s = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: C1_preserves_null_sets_open
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹⁴ : MetricSpace X
inst✝¹³ : MeasurableSpace X
inst✝¹² : BorelSpace X
inst✝¹¹ : MetricSpace Y
inst✝¹⁰ : MeasurableSpace Y
inst✝⁹ : BorelSpace Y
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : SigmaCompactSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
d : ℕ
s : Set E
hsU : s ⊆ U
hs : ↑μH[↑d] s = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
have : Convex ℝ U := sorry
Proof state after:
X : Type u_1
Y : Type u_2
inst✝¹⁴ : MetricSpace X
inst✝¹³ : MeasurableSpace X
inst✝¹² : BorelSpace X
inst✝¹¹ : MetricSpace Y
inst✝¹⁰ : MeasurableSpace Y
inst✝⁹ : BorelSpace Y
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : SigmaCompactSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
d : ℕ
s : Set E
hsU : s ⊆ U
hs : ↑μH[↑d] s = 0
this : Convex ℝ U
⊢ ↑μH[↑d] (f '' s) = 0
Theorem: C1_preserves_null_sets_open
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹⁴ : MetricSpace X
inst✝¹³ : MeasurableSpace X
inst✝¹² : BorelSpace X
inst✝¹¹ : MetricSpace Y
inst✝¹⁰ : MeasurableSpace Y
inst✝⁹ : BorelSpace Y
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : SigmaCompactSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
d : ℕ
s : Set E
hsU : s ⊆ U
hs : ↑μH[↑d] s = 0
this : Convex ℝ U
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
exact locally_lipschitz_image_of_null_set_is_null_set_open
  (LocallyLipschitz.of_C1_on_open hU this hf) hsU hs
Proof state after:
no goals
Theorem: empty_iff_open_cover
Proof state before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
⊢ s = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Tactic:
have : ⋃ (α : I), s ∩ U α = s := by rw [←inter_iUnion, hcover, inter_univ s]
Proof state after:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ s = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Theorem: empty_iff_open_cover
Proof state before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ s = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Tactic:
nth_rewrite 1 [← this]
Proof state after:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ ⋃ α, s ∩ U α = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Theorem: empty_iff_open_cover
Proof state before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ ⋃ α, s ∩ U α = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Tactic:
simp only [iUnion_eq_empty]
Proof state after:
no goals
Theorem: empty_iff_open_cover
Proof state before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
⊢ ⋃ α, s ∩ U α = s
Tactic:
rw [←inter_iUnion, hcover, inter_univ s]
Proof state after:
no goals
Theorem: image_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : PartialHomeomorph α β
s : Set α
⊢ e.target ∩ ↑e '' interior s = ↑e '' (e.source ∩ interior s)
Tactic:
sorry
Proof state after:
no goals
Theorem: homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
s : Set α
h₂s : interior s = ∅
⊢ interior (⇑f '' s) = ∅
Tactic:
rw [← Homeomorph.image_interior, h₂s]
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
s : Set α
h₂s : interior s = ∅
⊢ ⇑f '' ∅ = ∅
Theorem: homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
s : Set α
h₂s : interior s = ∅
⊢ ⇑f '' ∅ = ∅
Tactic:
exact Set.image_empty ↑f
Proof state after:
no goals
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
⊢ interior (↑f '' s) = ∅
Tactic:
have h₁ : s = s ∩ f.source := by
  rw [← @inter_eq_left α s f.source] at hs
  symm
  exact hs
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
⊢ interior (↑f '' s) = ∅
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
⊢ interior (↑f '' s) = ∅
Tactic:
have h₂ : interior s = interior (s ∩ f.source) := by
  sorry
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅
Tactic:
rw [h₁] at h₂s
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅
Tactic:
have h₃ : f '' (interior s ∩ f.source) = ∅ := by sorry
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
h₃ : ↑f '' (interior s ∩ f.source) = ∅
⊢ interior (↑f '' s) = ∅
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
h₃ : ↑f '' (interior s ∩ f.source) = ∅
⊢ interior (↑f '' s) = ∅
Tactic:
sorry
Proof state after:
no goals
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
⊢ s = s ∩ f.source
Tactic:
rw [← @inter_eq_left α s f.source] at hs
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s = s ∩ f.source
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s = s ∩ f.source
Tactic:
symm
Proof state after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s ∩ f.source = s
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s ∩ f.source = s
Tactic:
exact hs
Proof state after:
no goals
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
⊢ interior s = interior (s ∩ f.source)
Tactic:
sorry
Proof state after:
no goals
Theorem: local_homeo_preserves_empty_interior
Proof state before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ ↑f '' (interior s ∩ f.source) = ∅
Tactic:
sorry
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ interior s = ∅ ↔ ∀ (α : I), interior (s ∩ U α) = ∅
Tactic:
constructor
Proof state after:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ interior s = ∅ → ∀ (α : I), interior (s ∩ U α) = ∅

case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ (∀ (α : I), interior (s ∩ U α) = ∅) → interior s = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ interior s = ∅ → ∀ (α : I), interior (s ∩ U α) = ∅
Tactic:
intro hs α
Proof state after:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ interior (s ∩ U α) = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ interior (s ∩ U α) = ∅
Tactic:
have aux: interior (s ∩ U α) ⊆ interior s := by
  apply interior_mono
  apply Set.inter_subset_left
Proof state after:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
aux : interior (s ∩ U α) ⊆ interior s
⊢ interior (s ∩ U α) = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
aux : interior (s ∩ U α) ⊆ interior s
⊢ interior (s ∩ U α) = ∅
Tactic:
exact Set.subset_eq_empty aux hs
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ interior (s ∩ U α) ⊆ interior s
Tactic:
apply interior_mono
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ s ∩ U α ⊆ s
Theorem: interior_zero_iff_open_cover
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ s ∩ U α ⊆ s
Tactic:
apply Set.inter_subset_left
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ (∀ (α : I), interior (s ∩ U α) = ∅) → interior s = ∅
Tactic:
intro h
Proof state after:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ interior s = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ interior s = ∅
Tactic:
suffices ∀ V : Set X, (hV : V ⊆ s ∧ IsOpen V) → V = ∅ by sorry
Proof state after:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ ∀ (V : Set X), V ⊆ s ∧ IsOpen V → V = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ ∀ (V : Set X), V ⊆ s ∧ IsOpen V → V = ∅
Tactic:
rintro V ⟨hVS, hV⟩
Proof state after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
⊢ V = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
⊢ V = ∅
Tactic:
have h' : ∀ α : I, V ∩ U α = ∅ := by
  intro α
  have h₁ : IsOpen (V ∩ U α) := by exact IsOpen.inter hV (hU α)
  have h₂ : V ∩ U α ⊆ s ∩ U α := by exact Set.inter_subset_inter_left (U α) hVS
  have h₃ : V ∩ U α ⊆ interior (s ∩ U α) := by exact interior_maximal h₂ h₁
  exact Set.subset_eq_empty h₃ (h α)
Proof state after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
⊢ V = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
⊢ V = ∅
Tactic:
have h'' : V = ⋃ (α : I), (V ∩ U α) := by
  ext i
  rw [Set.mem_iUnion]
  sorry
Proof state after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ V = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ V = ∅
Tactic:
rw [h'']
Proof state after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ⋃ α, V ∩ U α = ∅