ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>x ⊔ xᶜ = ⊤
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>xᶜ ⊔ x = ⊤
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>IsCompl x xᶜ
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x \ y = x ⊓ yᶜ
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x ⇨ y = y ⊔ xᶜ
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>￢x = xᶜ
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>⊤ \ x = xᶜ
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x = yᶜ ↔ IsCompl x y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>xᶜ = y ↔ IsCompl x y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>xᶜ = y ↔ yᶜ = x
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x = yᶜ ↔ y = xᶜ
<VAR>α : Type u<VAR>BooleanAlgebra α<VAR>x : α<GOAL>xᶜᶜ = x
<VAR>α : Type u<VAR>BooleanAlgebra α<GOAL>compl ∘ compl = id
<VAR>α : Type u<VAR>BooleanAlgebra α<GOAL>Function.Involutive compl
<VAR>α : Type u<VAR>BooleanAlgebra α<GOAL>Function.Bijective compl
<VAR>α : Type u<VAR>BooleanAlgebra α<GOAL>Function.Surjective compl
<VAR>α : Type u<VAR>BooleanAlgebra α<GOAL>Function.Injective compl
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>xᶜ = yᶜ ↔ x = y
<VAR>α : Type u<VAR>x y z : α<VAR>BooleanAlgebra α<VAR>h : IsCompl x y<GOAL>zᶜ = y ↔ z = x
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>xᶜ = ⊤ ↔ x = ⊥
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>xᶜ = ⊥ ↔ x = ⊤
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>(x ⊓ y)ᶜ = xᶜ ⊔ yᶜ
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>yᶜ ≤ xᶜ ↔ x ≤ y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>yᶜ < xᶜ ↔ x < y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<VAR>h : yᶜ ≤ x<GOAL>xᶜ ≤ y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>xᶜ ≤ y ↔ yᶜ ≤ x
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>xᶜ ≤ x ↔ x = ⊤
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<VAR>Nontrivial α<GOAL>xᶜ < x ↔ x = ⊤
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x \ yᶜ = x ⊓ y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x ⊓ y ⊔ x ⊓ yᶜ = x
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>(x \ y)ᶜ = x ⇨ y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>(x ⇨ y)ᶜ = x \ y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>xᶜ \ yᶜ = y \ x
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>xᶜ ⇨ yᶜ = y ⇨ x
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>Disjoint xᶜ y ↔ y ≤ x
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>Disjoint x yᶜ ↔ x ≤ y
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>Codisjoint (x ⇨ y) x
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>Codisjoint x (x ⇨ y)
<VAR>α : Type u<VAR>x y z : α<VAR>BooleanAlgebra α<GOAL>x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x ⇨ y ≤ x ↔ x = ⊤
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
<VAR>α : Type u<VAR>x y : α<VAR>BooleanAlgebra α<GOAL>x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤
<GOAL>(fun x x_1 => x ⊔ x_1) = or
<GOAL>(fun x x_1 => x ⊓ x_1) = and
<VAR>α : Type u_2<VAR>l : Filter α<VAR>self : CountableInterFilter l<VAR>S : Set (Set α)<GOAL>S.Countable → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>S : Set (Set α)<VAR>hSc : S.Countable<GOAL>⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Countable ι<VAR>s : ι → Set α<GOAL>⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s : (i : ι) → i ∈ S → Set α<GOAL>⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Countable ι<VAR>p : α → ι → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>p : α → (i : ι) → i ∈ S → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Countable ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ≤ᶠ[l] t i<GOAL>⋃ i, s i ≤ᶠ[l] ⋃ i, t i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Countable ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i =ᶠ[l] t i<GOAL>⋃ i, s i =ᶠ[l] ⋃ i, t i
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi<GOAL>⋃ i, ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Countable ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ≤ᶠ[l] t i<GOAL>⋂ i, s i ≤ᶠ[l] ⋂ i, t i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Countable ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i =ᶠ[l] t i<GOAL>⋂ i, s i =ᶠ[l] ⋂ i, t i
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
<VAR>α : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi<GOAL>⋂ i, ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
<VAR>α : Type u_2<VAR>l : Set (Set α)<VAR>hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l<VAR>h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l<VAR>s : Set α<GOAL>s ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l
<VAR>α : Type u_2<VAR>l : Set (Set α)<VAR>hunion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l<VAR>hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l<VAR>s : Set α<GOAL>s ∈ Filter.ofCountableUnion l hunion hmono ↔ l sᶜ
<VAR>α : Type u_2<VAR>g : Set (Set α)<VAR>s : Set α<GOAL>s ∈ Filter.countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
<VAR>α : Type u_2<VAR>g : Set (Set α)<VAR>f : Filter α<VAR>CountableInterFilter f<GOAL>f ≤ Filter.countableGenerate g ↔ g ⊆ f.sets
<VAR>α : Type u_2<VAR>g : Set (Set α)<GOAL>IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (Filter.countableGenerate g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>TopologicalSpace β<VAR>l : Filter α<GOAL>l.ZeroAtFilter 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>AddZeroClass β<VAR>ContinuousAdd β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : l.ZeroAtFilter f<VAR>hg : l.ZeroAtFilter g<GOAL>l.ZeroAtFilter (f + g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>ContinuousNeg β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : l.ZeroAtFilter f<GOAL>l.ZeroAtFilter (-f)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>Zero 𝕜<VAR>Zero β<VAR>SMulWithZero 𝕜 β<VAR>ContinuousConstSMul 𝕜 β<VAR>l : Filter α<VAR>f : α → β<VAR>c : 𝕜<VAR>hf : l.ZeroAtFilter f<GOAL>l.ZeroAtFilter (c • f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NormedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : l.ZeroAtFilter f<GOAL>l.BoundedAtFilter f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Norm β<VAR>l : Filter α<VAR>c : β<GOAL>l.BoundedAtFilter (Function.const α c)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : l.BoundedAtFilter f<VAR>hg : l.BoundedAtFilter g<GOAL>l.BoundedAtFilter (f + g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : l.BoundedAtFilter f<GOAL>l.BoundedAtFilter (-f)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedRing 𝕜<VAR>SeminormedAddCommGroup β<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>l : Filter α<VAR>f : α → β<VAR>c : 𝕜<VAR>hf : l.BoundedAtFilter f<GOAL>l.BoundedAtFilter (c • f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedRing β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : l.BoundedAtFilter f<VAR>hg : l.BoundedAtFilter g<GOAL>l.BoundedAtFilter (f * g)
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>f.smallSets = Filter.generate (Set.powerset '' f.sets)
<VAR>α : Type u_1<GOAL>GaloisConnection (fun L => L.bind 𝓟) Filter.smallSets
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l.smallSets.HasBasis p fun i => 𝒫 s i
<VAR>α : Type u_1<VAR>l : Filter α<GOAL>l.smallSets.HasBasis (fun t => t ∈ l) Set.powerset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>f : α → Set β<GOAL>Filter.Tendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ (x : α) in la, f x ⊆ t
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : Set α → Prop<GOAL>(∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t ⊆ s, p t
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : Set α → Prop<VAR>hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s<GOAL>(∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, p s
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : Set α → Prop<GOAL>(∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s ⊆ t, p s
<VAR>α : Type u_1<VAR>l : Filter α<GOAL>∃ᶠ (s : Set α) in l.smallSets, s ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>f : α → β<GOAL>Filter.Tendsto (fun x => f '' x) la.smallSets lb.smallSets ↔ Filter.Tendsto f la lb
<VAR>α : Type u_1<VAR>l : Filter α<VAR>ι : Type u_4<VAR>Preorder ι<VAR>s : ι → Set α<VAR>hl : l.HasAntitoneBasis s<GOAL>Filter.Tendsto s Filter.atTop l.smallSets
<VAR>α : Type u_1<GOAL>Monotone Filter.smallSets
<VAR>α : Type u_1<GOAL>⊥.smallSets = pure ∅
<VAR>α : Type u_1<GOAL>⊤.smallSets = ⊤
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(𝓟 s).smallSets = 𝓟 (𝒫 s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter β<VAR>f : α → β<GOAL>(Filter.comap f l).smallSets = Filter.comap (Set.image f) l.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter β<VAR>f : α → β<GOAL>(Filter.comap f l).smallSets = l.lift' (Set.powerset ∘ Set.preimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter β<VAR>f : α → Set β<GOAL>Filter.comap f l.smallSets = l.lift' (Set.preimage f ∘ Set.powerset)
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>f : ι → Filter α<GOAL>(iInf f).smallSets = ⨅ i, (f i).smallSets
<VAR>α : Type u_1<VAR>l₁ l₂ : Filter α<GOAL>(l₁ ⊓ l₂).smallSets = l₁.smallSets ⊓ l₂.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>s t : α → Set β<VAR>ht : Filter.Tendsto t la lb.smallSets<VAR>hst : ∀ᶠ (x : α) in la, s x ⊆ t x<GOAL>Filter.Tendsto s la lb.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>s : α → Set β<VAR>f : α → β<VAR>hs : Filter.Tendsto s la lb.smallSets<VAR>hf : ∀ᶠ (x : α) in la, f x ∈ s x<GOAL>Filter.Tendsto f la lb
<VAR>α : Type u_1<VAR>l l' : Filter α<VAR>p : α → Prop<GOAL>(∀ᶠ (s : Set α) in l.smallSets, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : α → Prop<GOAL>(∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x
<VAR>α : Type u_1<VAR>l : Filter α<VAR>s : Set α<GOAL>(∀ᶠ (t : Set α) in l.smallSets, t ⊆ s) ↔ s ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>hs : s ∈ f<VAR>ht : t ∈ g<GOAL>s ×ˢ t ∈ f ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α × β)<VAR>f : Filter α<VAR>g : Filter β<GOAL>s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f.NeBot<VAR>g.NeBot<GOAL>s ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : Filter α<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>p : α × β → Prop<VAR>s : Set β<GOAL>(∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β × γ<VAR>b : Filter β<VAR>c : Filter γ<GOAL>Filter.comap f (b ×ˢ c) = Filter.comap (Prod.fst ∘ f) b ⊓ Filter.comap (Prod.snd ∘ f) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<GOAL>f ×ˢ ⊤ = Filter.comap Prod.fst f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : Filter β<GOAL>⊤ ×ˢ g = Filter.comap Prod.snd g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<GOAL>(f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<GOAL>(∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.Tendsto Prod.fst (f ×ˢ g) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.Tendsto Prod.snd (f ×ˢ g) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m : α → β × γ<VAR>H : Filter.Tendsto m f (g ×ˢ h)<GOAL>Filter.Tendsto (fun a => (m a).1) f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m : α → β × γ<VAR>H : Filter.Tendsto m f (g ×ˢ h)<GOAL>Filter.Tendsto (fun a => (m a).2) f h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m₁ : α → β<VAR>m₂ : α → γ<VAR>h₁ : Filter.Tendsto m₁ f g<VAR>h₂ : Filter.Tendsto m₂ f h<GOAL>Filter.Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.Tendsto Prod.swap (f ×ˢ g) (g ×ˢ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in la, p x<VAR>lb : Filter β<GOAL>∀ᶠ (x : α × β) in la ×ˢ lb, p x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>lb : Filter β<VAR>p : β → Prop<VAR>h : ∀ᶠ (x : β) in lb, p x<VAR>la : Filter α<GOAL>∀ᶠ (x : α × β) in la ×ˢ lb, p x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>pa : α → Prop<VAR>ha : ∀ᶠ (x : α) in la, pa x<VAR>lb : Filter β<VAR>pb : β → Prop<VAR>hb : ∀ᶠ (y : β) in lb, pb y<GOAL>∀ᶠ (p : α × β) in la ×ˢ lb, pa p.1 ∧ pb p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_6<VAR>la : Filter α<VAR>fa ga : α → γ<VAR>ha : fa =ᶠ[la] ga<VAR>lb : Filter β<VAR>fb gb : β → δ<VAR>hb : fb =ᶠ[lb] gb<GOAL>Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_6<VAR>LE γ<VAR>LE δ<VAR>la : Filter α<VAR>fa ga : α → γ<VAR>ha : fa ≤ᶠ[la] ga<VAR>lb : Filter β<VAR>fb gb : β → δ<VAR>hb : fb ≤ᶠ[lb] gb<GOAL>Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>p : α × β → Prop<VAR>h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x<GOAL>∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>p : α → β → Prop<VAR>h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y<GOAL>∃ᶠ (xy : α × β) in la ×ˢ lb, p xy.1 xy.2
<VAR>α : Type u_1<VAR>f : Filter α<VAR>p : α × α → Prop<VAR>h : ∀ᶠ (i : α × α) in f ×ˢ f, p i<GOAL>∀ᶠ (i : α) in f, p (i, i)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter γ<VAR>p : (α × α) × γ → Prop<GOAL>(∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter γ<VAR>p : α × γ × γ → Prop<GOAL>(∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>Filter.Tendsto (fun i => (i, i)) f (f ×ˢ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>Nonempty ι<VAR>f : ι → Filter α<VAR>g : Filter β<GOAL>(⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>Nonempty ι<VAR>f : Filter α<VAR>g : ι → Filter β<GOAL>f ×ˢ ⨅ i, g i = ⨅ i, f ×ˢ g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>hf : f₁ ≤ f₂<VAR>hg : g₁ ≤ g₂<GOAL>f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>hf : f₁ ≤ f₂<GOAL>f₁ ×ˢ g ≤ f₂ ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<VAR>hf : g₁ ≤ g₂<GOAL>f ×ˢ g₁ ≤ f ×ˢ g₂
<VAR>α₁ : Type u<VAR>α₂ : Type v<VAR>β₁ : Type w<VAR>β₂ : Type x<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>m₁ : β₁ → α₁<VAR>m₂ : β₂ → α₂<GOAL>Filter.comap m₁ f₁ ×ˢ Filter.comap m₂ f₂ = Filter.comap (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = Filter.comap Prod.swap (g ×ˢ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = Filter.map (fun p => (p.2, p.1)) (g ×ˢ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>g.NeBot<GOAL>Filter.map Prod.fst (f ×ˢ g) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>f.NeBot<GOAL>Filter.map Prod.snd (f ×ˢ g) = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>f₁.NeBot<VAR>g₁.NeBot<GOAL>f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>f₁.NeBot<VAR>g₁.NeBot<GOAL>f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<GOAL>(∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<GOAL>Filter.map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<GOAL>Filter.map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<GOAL>Filter.Tendsto (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) (f ×ˢ g ×ˢ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<GOAL>Filter.Tendsto (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) ((f ×ˢ g) ×ˢ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>k : Filter δ<GOAL>Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>k : Filter δ<GOAL>Filter.Tendsto (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) ((f ×ˢ h) ×ˢ g ×ˢ k)
<VAR>α₁ : Type u<VAR>α₂ : Type v<VAR>β₁ : Type w<VAR>β₂ : Type x<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>m₁ : α₁ → β₁<VAR>m₂ : α₂ → β₂<GOAL>Filter.map m₁ f₁ ×ˢ Filter.map m₂ f₂ = Filter.map (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>f : α₁ → α₂<VAR>g : β₁ → β₂<VAR>F : Filter α₁<VAR>G : Filter β₁<GOAL>Filter.map f F ×ˢ Filter.map g G = Filter.map (Prod.map f g) (F ×ˢ G)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter γ<GOAL>Filter.map f F ×ˢ G = Filter.map (Prod.map f id) (F ×ˢ G)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → γ<VAR>F : Filter α<VAR>G : Filter β<GOAL>F ×ˢ Filter.map f G = Filter.map (Prod.map id f) (F ×ˢ G)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter (α × β)<GOAL>f ≤ Filter.map Prod.fst f ×ˢ Filter.map Prod.snd f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_6<VAR>f : α → γ<VAR>g : β → δ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>d : Filter δ<VAR>hf : Filter.Tendsto f a c<VAR>hg : Filter.Tendsto g b d<GOAL>Filter.Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : α × β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map m (f ×ˢ g) = (Filter.map (fun a b => m (a, b)) f).seq g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = (Filter.map Prod.mk f).seq g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<GOAL>(f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>f : Filter β<GOAL>pure a ×ˢ f = Filter.map (Prod.mk a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>B : Filter β<GOAL>Filter.map (Function.uncurry f) (pure a ×ˢ B) = Filter.map (f a) B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>b : β<GOAL>f ×ˢ pure b = Filter.map (fun a => (a, b)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<GOAL>pure a ×ˢ pure b = pure (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<GOAL>f ×ˢ ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : Filter β<GOAL>⊥ ×ˢ g = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>hf : f.NeBot<VAR>hg : g.NeBot<GOAL>(f ×ˢ g).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>f' : Filter α<VAR>g' : Filter β<GOAL>Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>(∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α × β → γ<VAR>x : Filter α<VAR>y : Filter β<VAR>z : Filter γ<GOAL>Filter.Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>g' : Filter γ<VAR>s : α → β × γ<GOAL>Filter.Tendsto s f (g ×ˢ g') ↔ Filter.Tendsto (fun n => (s n).1) f g ∧ Filter.Tendsto (fun n => (s n).2) f g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter (α × β)<VAR>g : Filter α<VAR>g' : Filter β<GOAL>f ≤ g ×ˢ g' ↔ Filter.Tendsto Prod.fst f g ∧ Filter.Tendsto Prod.snd f g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α × β)<VAR>f : Filter α<VAR>g : Filter β<GOAL>s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter β<GOAL>⊥.coprod l = Filter.comap Prod.snd l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<GOAL>l.coprod ⊥ = Filter.comap Prod.fst l
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>⊥.coprod ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α × β)<VAR>la : Filter α<VAR>lb : Filter β<GOAL>sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>hf : f₁ ≤ f₂<VAR>hg : g₁ ≤ g₂<GOAL>f₁.coprod g₁ ≤ f₂.coprod g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>f.NeBot<VAR>Nonempty β<GOAL>(f.coprod g).NeBot