α : 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₂
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂
rw [rtendsto_def]
α : 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₂
α : 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₂
simp_rw [←l₂.mem_sets]
α : 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₁
α : 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₂
simp [Filter.le_def, rcomap, Rel.mem_image]
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₁

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₁
α : 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₁
constructor
no goals
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₁
exact fun h s t tl₂ => mem_of_superset (h t tl₂)
no goals
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₁
exact fun h t tl₂ => h _ t tl₂ Set.Subset.rfl