[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s t : Set α
Ixx : α → α → Set α
⊢ Tendsto (fun p => Ixx p.fst p.snd) (𝓟 s ×ˢ 𝓟 s) (smallSets (𝓟 t)) ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → Ixx x y ⊆ t
[PROOFSTEP]
simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal, forall_prod_set,
  mem_powerset_iff, mem_principal]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun p => Ixx p.fst p.snd) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (smallSets (l₂ ⊓ l₂'))
[PROOFSTEP]
simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ TendstoIxxClass Icc (pure a) (pure a)
[PROOFSTEP]
rw [← principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ TendstoIxxClass Icc (𝓟 {a}) (𝓟 {a})
[PROOFSTEP]
exact tendstoIxxClass_principal.2 ordConnected_singleton.out
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p => Ico p.fst p.snd) (pure a ×ˢ pure a) (smallSets ⊥)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p => Ioc p.fst p.snd) (pure a ×ˢ pure a) (smallSets ⊥)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p => Ioo p.fst p.snd) (pure a ×ˢ pure a) (smallSets ⊥)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
⊢ TendstoIxxClass uIcc l l
[PROOFSTEP]
refine' ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
⊢ ∃ t, t ∈ l ∧ t ×ˢ t ⊆ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
⊢ ∃ t, t ∈ l ∧ ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
⊢ ∃ t, t ∈ l ∧ t ×ˢ t ⊆ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
exact mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
⊢ ∃ t, t ∈ l ∧ t ×ˢ t ⊆ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
refine' ⟨t, htl, fun p hp => _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
⊢ p ∈ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
cases' le_total p.1 p.2 with h h
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.fst ≤ p.snd
⊢ p ∈ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, uIcc_of_le h]
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.fst ≤ p.snd
⊢ Icc p.fst p.snd ∈ s
[PROOFSTEP]
exact hts p hp
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.snd ≤ p.fst
⊢ p ∈ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, uIcc_of_ge h]
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.snd ≤ p.fst
⊢ Icc p.snd p.fst ∈ s
[PROOFSTEP]
exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩
