ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>l : ι → Filter α<VAR>p : (i : ι) → ι' i → Prop<VAR>s : (i : ι) → ι' i → Set α<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<GOAL>(⨅ i, l i).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If => ⋂ i ∈ If.1, s i (If.2 i)
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>l : ι → Filter α<VAR>p : (i : ι) → ι' i → Prop<VAR>s : (i : ι) → ι' i → Set α<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<GOAL>(⨅ i, l i).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), p (↑i) (If.snd i)) fun If => ⋂ i, s (↑i) (If.snd i)
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>Nonempty ι<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>h : Directed (fun x x_1 => x ≥ x_1) l<GOAL>(⨅ i, l i).HasBasis (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>Nonempty ι<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>h : Directed (fun x x_1 => x ≥ x_1) l<GOAL>(⨅ i, l i).HasBasis (fun ii' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<GOAL>(⨅ i ∈ dom, l i).HasBasis (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<GOAL>(⨅ i ∈ dom, l i).HasBasis (fun ii' => ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2
<VAR>α : Type u_1<VAR>t : Set α<GOAL>(𝓟 t).HasBasis (fun x => True) fun x => t
<VAR>α : Type u_1<VAR>x : α<GOAL>(pure x).HasBasis (fun x => True) fun x_1 => {x}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>(l ⊔ l').HasBasis (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∪ s' i.snd
<VAR>α : Type u_1<VAR>l l' : Filter α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>(l ⊔ l').HasBasis (fun i => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2
<VAR>α : Type u_1<VAR>ι : Sort u_6<VAR>ι' : ι → Type u_7<VAR>l : ι → Filter α<VAR>p : (i : ι) → ι' i → Prop<VAR>s : (i : ι) → ι' i → Set α<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<GOAL>(⨆ i, l i).HasBasis (fun f => ∀ (i : ι), p i (f i)) fun f => ⋃ i, s i (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>t : Set α<GOAL>(l ⊔ 𝓟 t).HasBasis p fun i => s i ∪ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>x : α<GOAL>(l ⊔ pure x).HasBasis p fun i => s i ∪ {x}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>s' : Set α<GOAL>(l ⊓ 𝓟 s').HasBasis p fun i => s i ∩ s'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>s' : Set α<GOAL>(𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>(l ⊓ l').NeBot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<GOAL>(l ⊓ l').NeBot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃s' : Set α⦄, s' ∈ l' → (s i ∩ s').Nonempty
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>t : Set α<GOAL>(l ⊓ 𝓟 t).NeBot ↔ ∀ ⦃i : ι⦄, p i → (s i ∩ t).Nonempty
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>h : Disjoint l l'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
<VAR>α : Type u_1<VAR>I : Type u_7<VAR>Finite I<VAR>l : I → Filter α<VAR>ι : I → Sort u_6<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>hd : Pairwise (Disjoint on l)<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))
<VAR>α : Type u_1<VAR>I : Type u_6<VAR>l : I → Filter α<VAR>ι : I → Sort u_7<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>S : Set I<VAR>hd : S.PairwiseDisjoint l<VAR>hS : S.Finite<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
<VAR>α : Type u_1<VAR>l l' : Filter α<GOAL>(l ⊓ l').NeBot ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s' : Set α⦄, s' ∈ l' → (s ∩ s').Nonempty
<VAR>α : Type u_1<VAR>l : Filter α<VAR>s : Set α<GOAL>(l ⊓ 𝓟 s).NeBot ↔ ∀ U ∈ l, (U ∩ s).Nonempty
<VAR>α : Type u_1<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥
<VAR>α : Type u_1<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∉ f ↔ (f ⊓ 𝓟 sᶜ).NeBot
<VAR>α : Type u_1<VAR>f : Filter α<VAR>s : Set α<GOAL>Disjoint f (𝓟 s) ↔ sᶜ ∈ f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>s : Set α<GOAL>Disjoint (𝓟 s) f ↔ sᶜ ∈ f
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>x y : α<GOAL>Disjoint (pure x) (pure y) ↔ x ≠ y
<VAR>α : Type u_1<VAR>l₁ l₂ : Filter α<GOAL>(Set.diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>Disjoint l' l ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'
<VAR>α : Type u_1<VAR>f g : Filter α<GOAL>f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥
<VAR>α : Type u_1<VAR>f g : Filter α<GOAL>(f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x
<VAR>α : Type u_1<VAR>f g : Filter α<GOAL>(f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l = ⨅ i, ⨅ (_ : p i), 𝓟 (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>s : ι → Set α<VAR>h : l.HasBasis (fun x => True) s<GOAL>l = ⨅ i, 𝓟 (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>h : Directed (fun x x_1 => x ≥ x_1) s<VAR>Nonempty ι<GOAL>(⨅ i, 𝓟 (s i)).HasBasis (fun x => True) s
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>s : ι → Set α<GOAL>(⨅ i, 𝓟 (s i)).HasBasis (fun t => t.Finite) fun t => ⋂ i ∈ t, s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : β → Set α<VAR>S : Set β<VAR>h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S<VAR>ne : S.Nonempty<GOAL>(⨅ i ∈ S, 𝓟 (s i)).HasBasis (fun i => i ∈ S) s
<VAR>α : Type u_1<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), p i → ∀ (j : ι), p j → ∃ k, p k ∧ s k ⊆ s i ∧ s k ⊆ s j<VAR>ne : ∃ i, p i<GOAL>(⨅ i, ⨅ (_ : p i), 𝓟 (s i)).HasBasis p s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : α → β<VAR>hl : l.HasBasis p s<GOAL>(Filter.map f l).HasBasis p fun i => f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : β → α<VAR>hl : l.HasBasis p s<GOAL>(Filter.comap f l).HasBasis p fun i => f ⁻¹' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : Filter β<GOAL>(Filter.comap f l).HasBasis (fun s => s ∈ l) fun s => f ⁻¹' s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<VAR>x : α<GOAL>(∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>CompleteLattice β<VAR>f : Set α → β<VAR>h : l.HasBasis p s<VAR>hf : Monotone f<GOAL>⨅ t ∈ l, f t = ⨅ i, ⨅ (_ : p i), f (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Set α → Set β<VAR>h : l.HasBasis p s<VAR>hf : Monotone f<GOAL>⋂ t ∈ l, f t = ⋂ i, ⋂ (_ : p i), f (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l.ker = ⋂ i, ⋂ (_ : p i), s i
<VAR>α : Type u_1<VAR>ι'' : Type u_6<VAR>Preorder ι''<VAR>s'' : ι'' → Set α<VAR>self : Filter.IsAntitoneBasis s''<GOAL>Antitone s''
<VAR>α : Type u_1<VAR>ι'' : Type u_6<VAR>Preorder ι''<VAR>l : Filter α<VAR>s : ι'' → Set α<VAR>self : l.HasAntitoneBasis s<GOAL>Antitone s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι'' : Type u_6<VAR>Preorder ι''<VAR>l : Filter α<VAR>s : ι'' → Set α<VAR>hf : l.HasAntitoneBasis s<VAR>m : α → β<GOAL>(Filter.map m l).HasAntitoneBasis fun x => m '' s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι'' : Type u_6<VAR>Preorder ι''<VAR>l : Filter α<VAR>s : ι'' → Set α<VAR>hf : l.HasAntitoneBasis s<VAR>m : β → α<GOAL>(Filter.comap m l).HasAntitoneBasis fun x => m ⁻¹' s x
<VAR>α : Type u_1<VAR>ι : Type u_7<VAR>Preorder ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : ι → Set α<VAR>hs : Antitone s<GOAL>(⨅ i, 𝓟 (s i)).HasAntitoneBasis s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>f : α → β<VAR>hla : la.HasBasis pa sa<GOAL>Filter.Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ Set.MapsTo f (sa i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hlb : lb.HasBasis pb sb<GOAL>Filter.Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hla : la.HasBasis pa sa<VAR>hlb : lb.HasBasis pb sb<GOAL>Filter.Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>f : α → β<VAR>H : Filter.Tendsto f la lb<VAR>hla : la.HasBasis pa sa<VAR>t : Set β<GOAL>t ∈ lb → ∃ i, pa i ∧ Set.MapsTo f (sa i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>H : Filter.Tendsto f la lb<VAR>hlb : lb.HasBasis pb sb<VAR>i : ι'<GOAL>pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>H : Filter.Tendsto f la lb<VAR>hla : la.HasBasis pa sa<VAR>hlb : lb.HasBasis pb sb<VAR>ib : ι'<GOAL>pb ib → ∃ ia, pa ia ∧ Set.MapsTo f (sa ia) (sb ib)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>hla : la.HasBasis pa sa<VAR>hlb : lb.HasBasis pb sb<GOAL>(la ×ˢ lb).HasBasis (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>hla : la.HasBasis pa sa<VAR>hlb : lb.HasBasis pb sb<GOAL>(la ×ˢ lb).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>la : Filter α<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>p : ι → Prop<VAR>sb : ι → Set β<VAR>hla : la.HasBasis p sa<VAR>hlb : lb.HasBasis p sb<VAR>h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j<GOAL>(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>ι : Type u_6<VAR>LinearOrder ι<VAR>p : ι → Prop<VAR>sa : ι → Set α<VAR>sb : ι → Set β<VAR>hla : la.HasBasis p sa<VAR>hlb : lb.HasBasis p sb<VAR>hsa : MonotoneOn sa {i | p i}<VAR>hsb : MonotoneOn sb {i | p i}<GOAL>(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>ι : Type u_6<VAR>LinearOrder ι<VAR>p : ι → Prop<VAR>sa : ι → Set α<VAR>sb : ι → Set β<VAR>hla : la.HasBasis p sa<VAR>hlb : lb.HasBasis p sb<VAR>hsa : AntitoneOn sa {i | p i}<VAR>hsb : AntitoneOn sb {i | p i}<GOAL>(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>hl : la.HasBasis pa sa<GOAL>(la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i
<VAR>α : Type u_1<VAR>la : Filter α<VAR>s : Set (α × α)<GOAL>s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s
<VAR>α : Type u_1<VAR>la : Filter α<VAR>r : α → α → Prop<GOAL>(∀ᶠ (x : α × α) in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_6<VAR>LinearOrder ι<VAR>f : Filter α<VAR>g : Filter β<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>hf : f.HasAntitoneBasis s<VAR>hg : g.HasAntitoneBasis t<GOAL>(f ×ˢ g).HasAntitoneBasis fun n => s n ×ˢ t n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>la : Filter α<VAR>lb : Filter β<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>hla : la.HasBasis pa sa<VAR>hlb : lb.HasBasis pb sb<GOAL>(la.coprod lb).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => Prod.fst ⁻¹' sa i.1 ∪ Prod.snd ⁻¹' sb i.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>π : α → Type u_6<VAR>π' : β → Type u_7<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : (a : α) → π a → π' (f a)<VAR>a : α<VAR>l : Filter (π' (f a))<GOAL>Filter.map (Sigma.mk a) (Filter.comap (g a) l) = Filter.comap (Sigma.map f g) (Filter.map (Sigma.mk (f a)) l)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>self : f.IsCountablyGenerated<GOAL>∃ s, s.Countable ∧ f = Filter.generate s
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>self : Filter.IsCountableBasis p s<GOAL>(setOf p).Countable
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>self : l.HasCountableBasis p s<GOAL>(setOf p).Countable
<VAR>α : Type u_6<VAR>self : Filter.CountableFilterBasis α<GOAL>self.sets.Countable
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : f.HasCountableBasis p s<GOAL>f.IsCountablyGenerated
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Countable ι<VAR>f : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : f.HasBasis p s<GOAL>f.IsCountablyGenerated
<VAR>α : Type u_1<VAR>s : ℕ → Set α<GOAL>∃ t, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>CompleteLattice α<VAR>B : Set ι<VAR>Bcbl : B.Countable<VAR>Bne : B.Nonempty<VAR>f : ι → α<GOAL>∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>CompleteLattice α<VAR>B : Set ι<VAR>Bcbl : B.Countable<VAR>f : ι → α<VAR>i₀ : ι<VAR>h : f i₀ = ⊤<GOAL>∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
<VAR>α : Type u_1<VAR>B : Set (Set α)<VAR>Bcbl : B.Countable<GOAL>∃ x, ⨅ t ∈ B, 𝓟 t = ⨅ i, 𝓟 (x i)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder ι<VAR>l : Filter α<VAR>s : ι → Set α<VAR>hs : l.HasAntitoneBasis s<VAR>t : Set α<GOAL>t ∈ l ↔ ∃ i, s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder ι<VAR>l : Filter α<VAR>s : ι → Set α<VAR>hs : l.HasAntitoneBasis s<VAR>i : ι<GOAL>s i ∈ l
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>l : Filter α<VAR>s : ι → Set α<VAR>hs : l.HasAntitoneBasis s<VAR>i : ι<GOAL>l.HasBasis (fun j => i ≤ j) s
<VAR>α : Type u_1<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>f.IsCountablyGenerated<GOAL>∃ x, f.HasAntitoneBasis x
<VAR>α : Type u_1<VAR>f : Filter α<VAR>f.IsCountablyGenerated<GOAL>∃ x, Antitone x ∧ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s
<VAR>α : Type u_1<VAR>ι' : Sort u_5<VAR>Countable ι'<VAR>x : ι' → Set α<GOAL>(⨅ i, 𝓟 (x i)).IsCountablyGenerated
<VAR>α : Type u_1<VAR>f : Filter α<VAR>h : ∃ x, f = ⨅ i, 𝓟 (x i)<GOAL>f.IsCountablyGenerated
<VAR>α : Type u_1<VAR>B : Set (Set α)<VAR>h : B.Countable<GOAL>(⨅ s ∈ B, 𝓟 s).IsCountablyGenerated
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>f.IsCountablyGenerated ↔ ∃ x, f.HasAntitoneBasis x
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(𝓟 s).IsCountablyGenerated
<VAR>α : Type u_1<VAR>a : α<GOAL>(pure a).IsCountablyGenerated
<VAR>α : Type u_1<GOAL>⊥.IsCountablyGenerated
<VAR>α : Type u_1<GOAL>⊤.IsCountablyGenerated
<VAR>α : Type u<VAR>l : Filter α<VAR>c : Cardinal.{u}<VAR>self : CardinalInterFilter l c<VAR>S : Set (Set α)<GOAL>#↑S < c → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>S : Set (Set α)<VAR>CardinalInterFilter l c<VAR>hSc : #↑S < c<GOAL>⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l
<VAR>α : Type u<VAR>l : Filter α<GOAL>CardinalInterFilter l ℵ₀
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>hc : ℵ₀ < c<GOAL>CountableInterFilter l
<VAR>α : Type u<VAR>l : Filter α<GOAL>CardinalInterFilter l (Cardinal.aleph 1) ↔ CountableInterFilter l
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>a : Cardinal.{u}<VAR>hac : a ≤ c<GOAL>CardinalInterFilter l a
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>a : Cardinal.{u}<VAR>hac : a < c<GOAL>CardinalInterFilter l a
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>s : ι → Set α<VAR>hic : #ι < c<GOAL>⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s : (i : ι) → i ∈ S → Set α<GOAL>⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>p : α → ι → Prop<VAR>hic : #ι < c<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<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>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>s t : ι → Set α<VAR>hic : #ι < c<VAR>h : ∀ (i : ι), s i ≤ᶠ[l] t i<GOAL>⋃ i, s i ≤ᶠ[l] ⋃ i, t i
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>s t : ι → Set α<VAR>hic : #ι < c<VAR>h : ∀ (i : ι), s i =ᶠ[l] t i<GOAL>⋃ i, s i =ᶠ[l] ⋃ i, t i
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<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<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<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<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>s t : ι → Set α<VAR>hic : #ι < c<VAR>h : ∀ (i : ι), s i ≤ᶠ[l] t i<GOAL>⋂ i, s i ≤ᶠ[l] ⋂ i, t i
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>s t : ι → Set α<VAR>hic : #ι < c<VAR>h : ∀ (i : ι), s i =ᶠ[l] t i<GOAL>⋂ i, s i =ᶠ[l] ⋂ i, t i
<VAR>ι α : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<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<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<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<VAR>c : Cardinal.{u}<VAR>l : Set (Set α)<VAR>hc : 2 < c<VAR>hl : ∀ (S : Set (Set α)), #↑S < c → S ⊆ l → ⋂₀ S ∈ l<VAR>h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l<VAR>s : Set α<GOAL>s ∈ Filter.ofCardinalInter l hc hl h_mono ↔ s ∈ l
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>l : Set (Set α)<VAR>hc : 2 < c<VAR>hunion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l<VAR>hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l<VAR>s : Set α<GOAL>s ∈ Filter.ofCardinalUnion l hc hunion hmono ↔ l sᶜ
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>g : Set (Set α)<VAR>hc : 2 < c<GOAL>CardinalInterFilter (Filter.cardinalGenerate g hc) c
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>g : Set (Set α)<VAR>s : Set α<VAR>hreg : c.IsRegular<GOAL>s ∈ Filter.cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>g : Set (Set α)<VAR>f : Filter α<VAR>CardinalInterFilter f c<VAR>hc : 2 < c<GOAL>f ≤ Filter.cardinalGenerate g hc ↔ g ⊆ f.sets
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>g : Set (Set α)<VAR>hc : 2 < c<GOAL>IsGreatest {f | CardinalInterFilter f c ∧ g ⊆ f.sets} (Filter.cardinalGenerate g hc)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : Set α → Filter β<GOAL>⊤.lift g = g Set.univ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<GOAL>∀ {s : Set γ}, s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<GOAL>(f.lift g).HasBasis (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<VAR>s : Set β<GOAL>s ∈ f.lift g ↔ ∃ t ∈ f, s ∈ g t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>s : Set β<VAR>t : Set α<VAR>ht : t ∈ f<VAR>hs : s ∈ g t<GOAL>s ∈ f.lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>h : Filter β<VAR>s : Set α<VAR>hs : s ∈ f<VAR>hg : g s ≤ h<GOAL>f.lift g ≤ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>h : Filter β<GOAL>h ≤ f.lift g ↔ ∀ s ∈ f, h ≤ g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Set α → Filter β<VAR>hf : f₁ ≤ f₂<VAR>hg : g₁ ≤ g₂<GOAL>f₁.lift g₁ ≤ f₂.lift g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g₁ g₂ : Set α → Filter β<VAR>hg : ∀ s ∈ f, g₁ s ≤ g₂ s<GOAL>f.lift g₁ ≤ f.lift g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>m : γ → β<VAR>l : Filter γ<GOAL>Filter.Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Filter.Tendsto m l (g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>m : β → γ<VAR>hg : Monotone g<GOAL>Filter.map m (f.lift g) = f.lift (Filter.map m ∘ g)