[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ 𝓝 0 = ⨅ (γ : Γ₀) (_ : γ ≠ 0), 𝓟 (Iio γ)
[PROOFSTEP]
rw [nhds_eq_update, update_same]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (𝓝 0) (fun γ => γ ≠ 0) Iio
[PROOFSTEP]
rw [nhds_zero]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (⨅ (γ : Γ₀) (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun γ => γ ≠ 0) Iio
[PROOFSTEP]
refine' hasBasis_biInf_principal _ ⟨1, one_ne_zero⟩
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ DirectedOn ((fun γ => Iio γ) ⁻¹'o fun x x_1 => x ≥ x_1) fun γ => γ = 0 → False
[PROOFSTEP]
exact directedOn_iff_directed.2 (directed_of_inf fun a b hab => Iio_subset_Iio hab)
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀
[PROOFSTEP]
simp [nhds_zero]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h₀ : γ ≠ 0
⊢ 𝓝 γ = pure γ
[PROOFSTEP]
rw [nhds_eq_update, update_noteq h₀]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀ˣ
⊢ {↑γ} ∈ 𝓝 ↑γ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : γ ≠ 0
⊢ {γ} ∈ 𝓝 γ
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (𝓝 x) (fun x => True) fun x_1 => {x}
[PROOFSTEP]
rw [nhds_of_ne_zero h]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (pure x) (fun x => True) fun x_1 => {x}
[PROOFSTEP]
exact hasBasis_pure _
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ
[PROOFSTEP]
rw [nhds_of_ne_zero h, tendsto_pure]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : γ₁ < γ₂
⊢ Iio γ₂ ∈ 𝓝 γ₁
[PROOFSTEP]
rcases eq_or_ne γ₁ 0 with (rfl | h₀)
[GOAL]
case inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : 0 < γ₂
⊢ Iio γ₂ ∈ 𝓝 0
[PROOFSTEP]
simp [*, h.ne', Iio_mem_nhds_zero]
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : γ₁ < γ₂
h₀ : γ₁ ≠ 0
⊢ Iio γ₂ ∈ 𝓝 γ₁
[PROOFSTEP]
simp [*, h.ne', Iio_mem_nhds_zero]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ IsOpen s ↔ ¬0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
[PROOFSTEP]
rw [isOpen_iff_mem_nhds, ← and_forall_ne (0 : Γ₀)]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ ¬0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
[PROOFSTEP]
simp (config := { contextual := true }) [nhds_of_ne_zero, imp_iff_not_or, hasBasis_nhds_zero.mem_iff]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ
[PROOFSTEP]
simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici, compl_subset_compl]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ IsClosed {p | p.fst ≤ p.snd}
[PROOFSTEP]
simp only [← isOpen_compl_iff, compl_setOf, not_le, isOpen_iff_mem_nhds]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ ∀ (a : Γ₀ × Γ₀), a ∈ {a | a.snd < a.fst} → {a | a.snd < a.fst} ∈ 𝓝 a
[PROOFSTEP]
rintro ⟨a, b⟩ (hab : b < a)
[GOAL]
case mk
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.snd < a.fst} ∈ 𝓝 (a, b)
[PROOFSTEP]
rw [nhds_prod_eq, nhds_of_ne_zero (zero_le'.trans_lt hab).ne', pure_prod]
[GOAL]
case mk
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.snd < a.fst} ∈ map (Prod.mk a) (𝓝 b)
[PROOFSTEP]
exact Iio_mem_nhds hab
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
by_cases hs : 0 ∈ s
[GOAL]
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
have ht : 0 ∉ t := fun ht => disjoint_left.1 h₁ (subset_closure hs) ht
[GOAL]
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
hs : 0 ∈ s
ht : ¬0 ∈ t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
rwa [(isOpen_iff.2 (.inl ht)).nhdsSet_eq, disjoint_nhdsSet_principal]
[GOAL]
case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
hs : ¬0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
rwa [(isOpen_iff.2 (.inl hs)).nhdsSet_eq, disjoint_principal_nhdsSet]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
simp only [continuous_iff_continuousAt, ContinuousAt]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ ∀ (x : Γ₀ × Γ₀), Tendsto (fun p => p.fst * p.snd) (𝓝 x) (𝓝 (x.fst * x.snd))
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case mk
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
wlog hle : x ≤ y generalizing x y
[GOAL]
case mk.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
hle : ¬x ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
have := (this y x (le_of_not_le hle)).comp (continuous_swap.tendsto (x, y))
[GOAL]
case mk.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this✝ : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
hle : ¬x ≤ y
this : Tendsto ((fun p => p.fst * p.snd) ∘ Prod.swap) (𝓝 (x, y)) (𝓝 ((y, x).fst * (y, x).snd))
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
simpa only [mul_comm, Function.comp, Prod.swap] using this
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, y)) (𝓝 ((0, y).fst * (0, y).snd))
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
skip
[GOAL]
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, 0)) (𝓝 ((0, 0).fst * (0, 0).snd))
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, 0)) (𝓝 0)
[PROOFSTEP]
refine
  ((hasBasis_nhds_zero.prod_nhds hasBasis_nhds_zero).tendsto_iff hasBasis_nhds_zero).2 fun γ hγ =>
    ⟨(γ, 1), ⟨hγ, one_ne_zero⟩, ?_⟩
[GOAL]
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
γ : Γ₀
hγ : γ ≠ 0
⊢ ∀ (x : Γ₀ × Γ₀), x ∈ Iio (γ, 1).fst ×ˢ Iio (γ, 1).snd → x.fst * x.snd ∈ Iio γ
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : x < γ, hy : y < 1⟩
[GOAL]
case inl.inl.mk.intro
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
γ : Γ₀
hγ : γ ≠ 0
x y : Γ₀
hx : x < γ
hy : y < 1
⊢ (x, y).fst * (x, y).snd ∈ Iio γ
[PROOFSTEP]
exact (mul_lt_mul₀ hx hy).trans_eq (mul_one γ)
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, y)) (𝓝 ((0, y).fst * (0, y).snd))
[PROOFSTEP]
rw [zero_mul, nhds_prod_eq, nhds_of_ne_zero hy, prod_pure, tendsto_map'_iff]
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto ((fun p => p.fst * p.snd) ∘ fun a => (a, y)) (𝓝 0) (𝓝 0)
[PROOFSTEP]
refine' (hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => _
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ ia, ia ≠ 0 ∧ ∀ (x : Γ₀), x ∈ Iio ia → ((fun p => p.fst * p.snd) ∘ fun a => (a, y)) x ∈ Iio γ
[PROOFSTEP]
refine' ⟨γ / y, div_ne_zero hγ hy, fun x hx => _⟩
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
x : Γ₀
hx : x ∈ Iio (γ / y)
⊢ ((fun p => p.fst * p.snd) ∘ fun a => (a, y)) x ∈ Iio γ
[PROOFSTEP]
calc
  x * y < γ / y * y := mul_lt_right₀ _ hx hy
  _ = γ := div_mul_cancel _ hy
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
have hy : y ≠ 0 := ((zero_lt_iff.mpr hx).trans_le hle).ne'
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
rw [nhds_prod_eq, nhds_of_ne_zero hx, nhds_of_ne_zero hy, prod_pure_pure]
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (pure (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
exact pure_le_nhds (x * y)
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ ContinuousAt Inv.inv γ
[PROOFSTEP]
rw [ContinuousAt, nhds_of_ne_zero h]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)
[PROOFSTEP]
exact pure_le_nhds γ⁻¹
