[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l : Filter α
⊢ Set.univ ∈ {s | Rel.core r s ∈ l}
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | Rel.core r s ∈ l}
ht : y✝ ∈ {s | Rel.core r s ∈ l}
⊢ x✝ ∩ y✝ ∈ {s | Rel.core r s ∈ l}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | Rel.core r s ∈ l}
ht : y✝ ∈ {s | Rel.core r s ∈ l}
⊢ Rel.core r (x✝ ∩ y✝) ∈ l
[PROOFSTEP]
convert inter_mem hs ht
[GOAL]
case h.e'_4
α : Type u
β : Type v
γ : Type w
r : Rel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | Rel.core r s ∈ l}
ht : y✝ ∈ {s | Rel.core r s ∈ l}
⊢ Rel.core r (x✝ ∩ y✝) = Rel.core r x✝ ∩ Rel.core r y✝
[PROOFSTEP]
rw [← Rel.core_inter]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter α
⊢ (rmap s (rmap r l)).sets = (rmap (Rel.comp r s) l).sets
[PROOFSTEP]
simp [rmap_sets, Set.preimage, Rel.core_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (Rel.comp r s) l).sets
[PROOFSTEP]
ext t
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (Rel.comp r s) l).sets
[PROOFSTEP]
simp [rcomap_sets, Rel.image, Rel.core_comp]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1, x_1 ∈ l ∧ Rel.core s x_1 ⊆ x) ∧ Rel.core r x ⊆ t) ↔ ∃ x, x ∈ l ∧ Rel.core r (Rel.core s x) ⊆ t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1, x_1 ∈ l ∧ Rel.core s x_1 ⊆ x) ∧ Rel.core r x ⊆ t) → ∃ x, x ∈ l ∧ Rel.core r (Rel.core s x) ⊆ t
[PROOFSTEP]
rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
[GOAL]
case h.mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : Rel.core r u ⊆ t
v : Set γ
vsets : v ∈ l
hv : Rel.core s v ⊆ u
⊢ ∃ x, x ∈ l ∧ Rel.core r (Rel.core s x) ⊆ t
[PROOFSTEP]
exact ⟨v, vsets, Set.Subset.trans (Rel.core_mono _ hv) h⟩
[GOAL]
case h.mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, x ∈ l ∧ Rel.core r (Rel.core s x) ⊆ t) → ∃ x, (∃ x_1, x_1 ∈ l ∧ Rel.core s x_1 ⊆ x) ∧ Rel.core r x ⊆ t
[PROOFSTEP]
rintro ⟨t, tsets, ht⟩
[GOAL]
case h.mpr.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t✝ : Set α
t : Set γ
tsets : t ∈ l
ht : Rel.core r (Rel.core s t) ⊆ t✝
⊢ ∃ x, (∃ x_1, x_1 ∈ l ∧ Rel.core s x_1 ⊆ x) ∧ Rel.core r x ⊆ t✝
[PROOFSTEP]
exact ⟨Rel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂
[PROOFSTEP]
rw [rtendsto_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → Rel.core r s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
[PROOFSTEP]
simp_rw [← l₂.mem_sets]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂.sets → Rel.core r s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
[PROOFSTEP]
simp [Filter.le_def, rcomap, Rel.mem_image]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → Rel.core r s ∈ l₁) ↔ ∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.core r x_1 ⊆ x → x ∈ l₁
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → Rel.core r s ∈ l₁) → ∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.core r x_1 ⊆ x → x ∈ l₁
[PROOFSTEP]
exact fun h s t tl₂ => mem_of_superset (h t tl₂)
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.core r x_1 ⊆ x → x ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → Rel.core r s ∈ l₁
[PROOFSTEP]
exact fun h t tl₂ => h _ t tl₂ Set.Subset.rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (Rel.comp r s) l
[PROOFSTEP]
simp only [mem_rcomap', Rel.preimage_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t) ↔
    ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t) →
    ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
[PROOFSTEP]
rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : Rel.preimage r u ⊆ t
v : Set γ
vsets : v ∈ l
hv : Rel.preimage s v ⊆ u
⊢ ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
[PROOFSTEP]
exact ⟨v, vsets, (Rel.preimage_mono _ hv).trans h⟩
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t) →
    ∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t
[PROOFSTEP]
rintro ⟨t, tsets, ht⟩
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t✝ : Set α
t : Set γ
tsets : t ∈ l
ht : Rel.preimage r (Rel.preimage s t) ⊆ t✝
⊢ ∃ t, (∃ t_1, t_1 ∈ l ∧ Rel.preimage s t_1 ⊆ t) ∧ Rel.preimage r t ⊆ t✝
[PROOFSTEP]
exact ⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto' r l₁ l₂ ↔ ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
[PROOFSTEP]
unfold RTendsto' rcomap'
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets,
        univ_sets := (_ : ∃ x, x ∈ l₂.sets ∧ (fun s t => Rel.preimage r s ⊆ t) x Set.univ),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                x ⊆ y → y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                  x ∩ y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets) } ↔
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
[PROOFSTEP]
simp [le_def, Rel.mem_image]
[GOAL]
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁) ↔
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁) →
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
[PROOFSTEP]
exact fun h s hs => h _ _ hs Set.Subset.rfl
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁) →
    ∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁
[PROOFSTEP]
exact fun h s t ht => mem_of_superset (h t ht)
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂
[PROOFSTEP]
simp [tendsto_def, Function.graph, rtendsto_def, Rel.core, Set.preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂
[PROOFSTEP]
simp [tendsto_def, Function.graph, rtendsto'_def, Rel.preimage_def, Set.preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)
[PROOFSTEP]
ext t
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
[PROOFSTEP]
simp only [PFun.core_res, mem_pmap, mem_map, mem_inf_principal, imp_iff_not_or]
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | ¬x ∈ s ∨ x ∈ f ⁻¹' t} ∈ l
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
s : Set α
f : α → β
⊢ Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂
[PROOFSTEP]
simp only [Tendsto, PTendsto, pmap_res]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂
[PROOFSTEP]
rw [← tendsto_iff_ptendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
[PROOFSTEP]
simp [principal_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto' f l₁ l₂ → PTendsto f l₁ l₂
[PROOFSTEP]
rw [ptendsto_def, ptendsto'_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → PFun.preimage f s ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
[PROOFSTEP]
exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
⊢ PTendsto f l₁ l₂ → PTendsto' f l₁ l₂
[PROOFSTEP]
rw [ptendsto_def, ptendsto'_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
⊢ (∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → PFun.preimage f s ∈ l₁
[PROOFSTEP]
intro h' s sl₂
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
h' : ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ PFun.preimage f s ∈ l₁
[PROOFSTEP]
rw [PFun.preimage_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
h' : ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ PFun.core f s ∩ PFun.Dom f ∈ l₁
[PROOFSTEP]
exact inter_mem (h' s sl₂) h
