ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>r s : α → α → Prop<GOAL>Subrelation r s ↔ r ≤ s
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LE α<VAR>ha : ∀ (h : p), 0 ≤ a h<VAR>hb : ∀ (h : ¬p), 0 ≤ b h<GOAL>0 ≤ dite p a b
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LE α<VAR>ha : ∀ (h : p), 1 ≤ a h<VAR>hb : ∀ (h : ¬p), 1 ≤ b h<GOAL>1 ≤ dite p a b
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LE α<VAR>ha : ∀ (h : p), a h ≤ 0<VAR>hb : ∀ (h : ¬p), b h ≤ 0<GOAL>dite p a b ≤ 0
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LE α<VAR>ha : ∀ (h : p), a h ≤ 1<VAR>hb : ∀ (h : ¬p), b h ≤ 1<GOAL>dite p a b ≤ 1
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LT α<VAR>ha : ∀ (h : p), 0 < a h<VAR>hb : ∀ (h : ¬p), 0 < b h<GOAL>0 < dite p a b
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LT α<VAR>ha : ∀ (h : p), 1 < a h<VAR>hb : ∀ (h : ¬p), 1 < b h<GOAL>1 < dite p a b
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LT α<VAR>ha : ∀ (h : p), a h < 0<VAR>hb : ∀ (h : ¬p), b h < 0<GOAL>dite p a b < 0
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>LT α<VAR>ha : ∀ (h : p), a h < 1<VAR>hb : ∀ (h : ¬p), b h < 1<GOAL>dite p a b < 1
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LE α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>1 ≤ if p then a else b
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LE α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ if p then a else b
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LE α<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>(if p then a else b) ≤ 0
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LE α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<GOAL>(if p then a else b) ≤ 1
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LT α<VAR>ha : 1 < a<VAR>hb : 1 < b<GOAL>1 < if p then a else b
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LT α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < if p then a else b
<VAR>α : Type u_2<VAR>One α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LT α<VAR>ha : a < 1<VAR>hb : b < 1<GOAL>(if p then a else b) < 1
<VAR>α : Type u_2<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LT α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>(if p then a else b) < 0
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>Preorder β<VAR>f g : α → β<GOAL>↑f < ↑g ↔ ∀ᶠ (x : α) in ↑φ, f x < g x
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>Preorder β<VAR>Zero β<VAR>f : α → β<GOAL>0 < ↑f ↔ ∀ᶠ (x : α) in ↑φ, 0 < f x
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>Preorder β<VAR>x y : β<GOAL>x < y → ↑x < ↑y
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>Preorder β<VAR>x y : β<GOAL>↑x < ↑y ↔ x < y
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>Preorder β<GOAL>(fun x x_1 => x < x_1) = Filter.Germ.LiftRel fun x x_1 => x < x_1
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>LinearOrder β<VAR>x y : (↑φ).Germ β<GOAL>max x y = Filter.Germ.map₂ max x y
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>K : LinearOrder β<VAR>x y : (↑φ).Germ β<GOAL>min x y = Filter.Germ.map₂ min x y
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>LinearOrderedAddCommGroup β<VAR>x : (↑φ).Germ β<GOAL>|x| = Filter.Germ.map abs x
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>LinearOrder β<VAR>x y : β<GOAL>↑(max x y) = max ↑x ↑y
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>LinearOrder β<VAR>x y : β<GOAL>↑(min x y) = min ↑x ↑y
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>LinearOrderedAddCommGroup β<VAR>x : β<GOAL>↑|x| = |↑x|
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>P.IsEquipartition ↔ ∀ a ∈ P.parts, a.card = s.card / P.parts.card ∨ a.card = s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>¬P.IsEquipartition ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, b.card + 1 < a.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>h : (↑P.parts).Subsingleton<GOAL>P.IsEquipartition
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>t.card = s.card / P.parts.card ↔ t.card ≠ s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>s.card / P.parts.card ≤ t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>t.card ≤ s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>Finset.filter (fun p => ¬p.card = s.card / P.parts.card + 1) P.parts = Finset.filter (fun p => p.card = s.card / P.parts.card) P.parts
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>(Finset.filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).card = s.card % P.parts.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>(Finset.filter (fun p => p.card = s.card / P.parts.card) P.parts).card = P.parts.card - s.card % P.parts.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>∃ f, ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>⊥.IsEquipartition
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>Decidable (s = ⊥)<GOAL>⊤.IsEquipartition
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>hs : s ≠ ∅<GOAL>(Finpartition.indiscrete hs).IsEquipartition
<VAR>α : Type u<VAR>β : Type v<VAR>MulZeroClass β<VAR>PartialOrder β<VAR>PosMulMono β<VAR>MulPosMono β<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<VAR>hg₀ : 0 ≤ᶠ[l] g₁<VAR>hf₀ : 0 ≤ᶠ[l] f₂<GOAL>f₁ * g₁ ≤ᶠ[l] f₂ * g₂
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>Preorder β<VAR>CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass β β (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<GOAL>f₁ * g₁ ≤ᶠ[l] f₂ * g₂
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>Preorder β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<GOAL>f₁ + g₁ ≤ᶠ[l] f₂ + g₂
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedSemiring β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : 0 ≤ᶠ[l] f<VAR>hg : 0 ≤ᶠ[l] g<GOAL>0 ≤ᶠ[l] f * g
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedRing β<VAR>l : Filter α<VAR>f g : α → β<GOAL>0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>self : HasCountableSeparatingOn α p t<GOAL>∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>h : HasCountableSeparatingOn α p t<GOAL>∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>s₀ : Set α<VAR>hp : p s₀<VAR>t : Set α<VAR>HasCountableSeparatingOn α p t<GOAL>∃ S, S.Nonempty ∧ S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>s₀ : Set α<VAR>hp : p s₀<VAR>t : Set α<VAR>HasCountableSeparatingOn α p t<GOAL>∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
<VAR>α : Type u_1<VAR>p₁ p₂ : Set α → Prop<VAR>t₁ t₂ : Set α<VAR>h : HasCountableSeparatingOn α p₁ t₁<VAR>hp : ∀ (s : Set α), p₁ s → p₂ s<VAR>ht : t₂ ⊆ t₁<GOAL>HasCountableSeparatingOn α p₂ t₂
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>q : Set ↑t → Prop<VAR>h : HasCountableSeparatingOn (↑t) q Set.univ<VAR>hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U<GOAL>HasCountableSeparatingOn α p t
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<GOAL>HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) Set.univ ↔ HasCountableSeparatingOn α p t
<VAR>α : Type u_1<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>p : Set α → Prop<VAR>s : Set α<VAR>h : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
<VAR>α : Type u_1<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>p : Set α → Prop<VAR>s : Set α<VAR>HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hne : s.Nonempty<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ a ∈ s, {a} ∈ l
<VAR>α : Type u_1<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Nonempty α<VAR>p : Set α → Prop<VAR>s : Set α<VAR>HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ a, {a} ∈ l
<VAR>α : Type u_1<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>p : Set α → Prop<VAR>HasCountableSeparatingOn α p Set.univ<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ s, s.Subsingleton ∧ s ∈ l
<VAR>α : Type u_1<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>Nonempty α<VAR>p : Set α → Prop<VAR>HasCountableSeparatingOn α p Set.univ<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ x, {x} ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f : α → β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>HasCountableSeparatingOn β p s<VAR>hs : ∀ᶠ (x : α) in l, f x ∈ s<VAR>hne : s.Nonempty<VAR>h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U<GOAL>∃ a ∈ s, f =ᶠ[l] Function.const α a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f : α → β<VAR>Nonempty β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>HasCountableSeparatingOn β p s<VAR>hs : ∀ᶠ (x : α) in l, f x ∈ s<VAR>h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U<GOAL>∃ a, f =ᶠ[l] Function.const α a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f : α → β<VAR>Nonempty β<VAR>p : Set β → Prop<VAR>HasCountableSeparatingOn β p Set.univ<VAR>h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U<GOAL>∃ a, f =ᶠ[l] Function.const α a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>h' : HasCountableSeparatingOn β p s<VAR>hf : ∀ᶠ (x : α) in l, f x ∈ s<VAR>hg : ∀ᶠ (x : α) in l, g x ∈ s<VAR>h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>HasCountableSeparatingOn β p Set.univ<VAR>h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>HasCountableSeparatingOn β p s<VAR>hf : ∀ᶠ (x : α) in l, f x ∈ s<VAR>hg : ∀ᶠ (x : α) in l, g x ∈ s<VAR>h : ∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>HasCountableSeparatingOn β p Set.univ<VAR>h : ∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U<GOAL>f =ᶠ[l] g
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>l : Filter α<GOAL>(Filter.rmap r l).sets = r.core ⁻¹' l.sets
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>l : Filter α<VAR>s : Set β<GOAL>s ∈ Filter.rmap r l ↔ r.core s ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter α<GOAL>Filter.rmap s (Filter.rmap r l) = Filter.rmap (r.comp s) l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<GOAL>Filter.rmap s ∘ Filter.rmap r = Filter.rmap (r.comp s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.RTendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>f : Filter β<GOAL>(Filter.rcomap r f).sets = Rel.image (fun s t => r.core s ⊆ t) f.sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<GOAL>Filter.rcomap r (Filter.rcomap s l) = Filter.rcomap (r.comp s) l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<GOAL>Filter.rcomap r ∘ Filter.rcomap s = Filter.rcomap (r.comp s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.RTendsto r l₁ l₂ ↔ l₁ ≤ Filter.rcomap r l₂
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>l : Filter β<VAR>s : Set α<GOAL>s ∈ Filter.rcomap' r l ↔ ∃ t ∈ l, r.preimage t ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>f : Filter β<GOAL>(Filter.rcomap' r f).sets = Rel.image (fun s t => r.preimage s ⊆ t) f.sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<GOAL>Filter.rcomap' r (Filter.rcomap' s l) = Filter.rcomap' (r.comp s) l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<GOAL>Filter.rcomap' r ∘ Filter.rcomap' s = Filter.rcomap' (r.comp s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : Rel α β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Filter.Tendsto f l₁ l₂ ↔ Filter.RTendsto (Function.graph f) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Filter.Tendsto f l₁ l₂ ↔ Filter.RTendsto' (Function.graph f) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α →. β<VAR>l : Filter α<VAR>s : Set β<GOAL>s ∈ Filter.pmap f l ↔ f.core s ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.PTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f.core s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α →. β<GOAL>Filter.PTendsto f l₁ l₂ ↔ Filter.RTendsto f.graph' l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>s : Set α<VAR>f : α → β<GOAL>Filter.pmap (PFun.res f s) l = Filter.map f (l ⊓ Filter.principal s)
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>s : Set α<VAR>f : α → β<GOAL>Filter.Tendsto f (l₁ ⊓ Filter.principal s) l₂ ↔ Filter.PTendsto (PFun.res f s) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Filter.Tendsto f l₁ l₂ ↔ Filter.PTendsto (PFun.res f Set.univ) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.PTendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.PTendsto' f l₁ l₂ → Filter.PTendsto f l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : f.Dom ∈ l₁<GOAL>Filter.PTendsto f l₁ l₂ → Filter.PTendsto' f l₁ l₂
<VAR>α : Type u_1<VAR>l : Filter α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l.Subsingleton ↔ ∃ i, p i ∧ (s i).Subsingleton
<VAR>α : Type u_1<VAR>l l' : Filter α<VAR>hl : l.Subsingleton<VAR>hl' : l' ≤ l<GOAL>l'.Subsingleton
<VAR>α : Type u_1<VAR>l : Filter α<VAR>Subsingleton α<GOAL>l.Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>hl : l.Subsingleton<VAR>f : α → β<GOAL>(Filter.map f l).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>hl : l.Subsingleton<VAR>l' : Filter β<VAR>hl' : l'.Subsingleton<GOAL>(l ×ˢ l').Subsingleton
<VAR>α : Type u_1<VAR>a : α<GOAL>(pure a).Subsingleton
<VAR>α : Type u_1<GOAL>⊥.Subsingleton
<VAR>α : Type u_1<VAR>l : Filter α<VAR>l.NeBot<VAR>hl : l.Subsingleton<GOAL>∃ a, l = pure a
<VAR>α : Type u_1<VAR>l : Filter α<GOAL>l.Subsingleton ↔ l = ⊥ ∨ ∃ a, l = pure a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>Nonempty α<GOAL>l.Subsingleton ↔ ∃ a, l ≤ pure a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>Nonempty α<GOAL>l.Subsingleton ↔ ∃ a, {a} ∈ l
<VAR>α : Type u_1<VAR>l : Filter α<VAR>hl : l.Subsingleton<GOAL>l.IsCountablyGenerated
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>i : ι<GOAL>Filter.Tendsto (Function.eval i) (Filter.pi f) (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>β : Type u_3<VAR>m : β → (i : ι) → α i<VAR>l : Filter β<GOAL>Filter.Tendsto m l (Filter.pi f) ↔ ∀ (i : ι), Filter.Tendsto (fun x => m x i) l (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>g : Filter ((i : ι) → α i)<GOAL>g ≤ Filter.pi f ↔ ∀ (i : ι), Filter.Tendsto (Function.eval i) g (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f₁ f₂ : (i : ι) → Filter (α i)<VAR>h : ∀ (i : ι), f₁ i ≤ f₂ i<GOAL>Filter.pi f₁ ≤ Filter.pi f₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : s ∈ f i<GOAL>Function.eval i ⁻¹' s ∈ Filter.pi f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>h : ∀ i ∈ I, s i ∈ f i<GOAL>I.pi s ∈ Filter.pi f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>s ∈ Filter.pi f ↔ ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>s ∈ Filter.pi f ↔ ∃ I t, (∀ (i : ι), t i ∈ f i) ∧ (↑I).pi t ⊆ s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>∀ (i : ι), (f i).NeBot<VAR>I : Set ι<VAR>h : I.pi s ∈ Filter.pi f<VAR>i : ι<VAR>hi : i ∈ I<GOAL>s i ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>∀ (i : ι), (f i).NeBot<VAR>I : Set ι<VAR>hI : I.Finite<GOAL>I.pi s ∈ Filter.pi f ↔ ∀ i ∈ I, s i ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>p : (i : ι) → α i → Prop<VAR>i : ι<VAR>hf : ∀ᶠ (x : α i) in f i, p i x<GOAL>∀ᶠ (x : (i : ι) → α i) in Filter.pi f, p i (x i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>p : (i : ι) → α i → Prop<VAR>Finite ι<VAR>hf : ∀ (i : ι), ∀ᶠ (x : α i) in f i, p i x<GOAL>∀ᶠ (x : (i : ι) → α i) in Filter.pi f, ∀ (i : ι), p i (x i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>ι' : ι → Type<VAR>s : (i : ι) → ι' i → Set (α i)<VAR>p : (i : ι) → ι' i → Prop<VAR>h : ∀ (i : ι), (f i).HasBasis (p i) (s i)<GOAL>(Filter.pi f).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If => If.1.pi fun i => s i (If.2 i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : (i : ι) → Set (α i)<GOAL>𝓟 (Set.univ.pi s) ≤ Filter.pi fun i => 𝓟 (s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Finite ι<VAR>s : (i : ι) → Set (α i)<GOAL>(Filter.pi fun i => 𝓟 (s i)) = 𝓟 (Set.univ.pi s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Finite ι<VAR>f : (i : ι) → α i<GOAL>(Filter.pi fun x => pure (f x)) = pure f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<GOAL>Filter.pi f ⊓ 𝓟 (Set.univ.pi s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>∀ (i : ι), (f i).NeBot<VAR>I : Set ι<GOAL>Filter.pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<GOAL>(Filter.pi f ⊓ 𝓟 (Set.univ.pi s)).NeBot ↔ ∀ (i : ι), (f i ⊓ 𝓟 (s i)).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>∀ (i : ι), (f i).NeBot<VAR>I : Set ι<GOAL>(Filter.pi f ⊓ 𝓟 (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ 𝓟 (s i)).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<GOAL>Filter.pi f = ⊥ ↔ ∃ i, f i = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<GOAL>(Filter.pi f).NeBot ↔ ∀ (i : ι), (f i).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>∀ (i : ι), (f i).NeBot<VAR>i : ι<GOAL>Filter.map (Function.eval i) (Filter.pi f) = f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f₁ f₂ : (i : ι) → Filter (α i)<VAR>∀ (i : ι), (f₁ i).NeBot<GOAL>Filter.pi f₁ ≤ Filter.pi f₂ ↔ ∀ (i : ι), f₁ i ≤ f₂ i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f₁ f₂ : (i : ι) → Filter (α i)<VAR>∀ (i : ι), (f₁ i).NeBot<GOAL>Filter.pi f₁ = Filter.pi f₂ ↔ f₁ = f₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>s ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), ∃ t₁ ∈ f i, Function.eval i ⁻¹' t₁ ⊆ s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>sᶜ ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), (Function.eval i '' s)ᶜ ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<GOAL>(Filter.coprodᵢ f).NeBot ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ d, (f d).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>∀ (i : ι), Nonempty (α i)<GOAL>(Filter.coprodᵢ f).NeBot ↔ ∃ d, (f d).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<GOAL>Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>∀ (i : ι), Nonempty (α i)<GOAL>Filter.coprodᵢ f = ⊥ ↔ f = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<GOAL>Filter.coprodᵢ ⊥ = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<GOAL>(Filter.coprodᵢ fun x => ⊥) = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>∀ (i : ι), Nonempty (α i)<VAR>i : ι<VAR>h : (f i).NeBot<GOAL>(Filter.coprodᵢ f).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>∀ (i : ι), Nonempty (α i)<VAR>Nonempty ι<VAR>f : (i : ι) → Filter (α i)<VAR>H : ∀ (i : ι), (f i).NeBot<GOAL>(Filter.coprodᵢ f).NeBot
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f₁ f₂ : (i : ι) → Filter (α i)<VAR>hf : ∀ (i : ι), f₁ i ≤ f₂ i<GOAL>Filter.coprodᵢ f₁ ≤ Filter.coprodᵢ f₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>β : ι → Type u_3<VAR>m : (i : ι) → α i → β i<GOAL>Filter.map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => Filter.map (m i) (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → Filter (α i)<VAR>β : ι → Type u_3<VAR>m : (i : ι) → α i → β i<VAR>g : (i : ι) → Filter (β i)<VAR>h : ∀ (i : ι), Filter.Tendsto (m i) (f i) (g i)<GOAL>Filter.Tendsto (fun k i => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>l.NeBot<VAR>a b : β<GOAL>(∀ᶠ (x : α) in l, a = b) ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>l.NeBot<VAR>a b : β<GOAL>((fun x => a) =ᶠ[l] fun x => b) ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : Filter α<VAR>b : β<VAR>h : ∀ (x' : α), f x' = b<GOAL>(↑f).IsConstant
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>b : β<GOAL>(↑fun x => b).IsConstant
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>g : β → γ<VAR>h : (↑f).IsConstant<GOAL>(↑(g ∘ f)).IsConstant
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<GOAL>Quot.mk Setoid.r f = ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<GOAL>Quotient.mk' f = ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : l.Germ β<VAR>p : l.Germ β → Prop<VAR>h : ∀ (f : α → β), p ↑f<GOAL>p f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : l.Germ β<VAR>g : l.Germ γ<VAR>p : l.Germ β → l.Germ γ → Prop<VAR>h : ∀ (f : α → β) (g : α → γ), p ↑f ↑g<GOAL>p f g