ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>s : TopologicalSpace.Opens α<GOAL>IsCoatom s ↔ ∃ x, s = (TopologicalSpace.Closeds.singleton x).compl
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.Clopens α<GOAL>IsClopen self.carrier
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Clopens α<GOAL>IsClopen ↑s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Clopens α<GOAL>↑s.toOpens = ↑s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Clopens α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsClopen s<GOAL>↑{ carrier := s, isClopen' := h } = s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>x : α<VAR>h : IsClopen s<GOAL>x ∈ { carrier := s, isClopen' := h } ↔ x ∈ s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Clopens α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Clopens α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Clopens α<GOAL>↑(s \ t) = ↑s \ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Clopens α<GOAL>↑(s ⇨ t) = ↑s ⇨ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Clopens α<GOAL>↑sᶜ = (↑s)ᶜ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : TopologicalSpace.Clopens α<VAR>t : TopologicalSpace.Clopens β<VAR>x : α × β<GOAL>x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.IrreducibleCloseds α<GOAL>IsClosed self.carrier
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.IrreducibleCloseds α<GOAL>IsIrreducible self.carrier
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.IrreducibleCloseds α<GOAL>IsIrreducible ↑s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.IrreducibleCloseds α<GOAL>IsClosed ↑s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.IrreducibleCloseds α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsIrreducible s<VAR>h' : IsClosed s<GOAL>↑{ carrier := s, is_irreducible' := h, is_closed' := h' } = s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>x : α<GOAL>↑(TopologicalSpace.IrreducibleCloseds.singleton x) = {x}
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>a b : α<GOAL>a ∈ TopologicalSpace.IrreducibleCloseds.singleton b ↔ a = b
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>a : { x // IsIrreducible x ∧ IsClosed x }<GOAL>TopologicalSpace.IrreducibleCloseds.equivSubtype.symm a = { carrier := ↑a, is_irreducible' := ⋯, is_closed' := ⋯ }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>a : TopologicalSpace.IrreducibleCloseds α<GOAL>TopologicalSpace.IrreducibleCloseds.equivSubtype a = ⟨a.carrier, ⋯⟩
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>a : TopologicalSpace.IrreducibleCloseds α<GOAL>TopologicalSpace.IrreducibleCloseds.equivSubtype' a = ⟨a.carrier, ⋯⟩
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>a : { x // IsClosed x ∧ IsIrreducible x }<GOAL>TopologicalSpace.IrreducibleCloseds.equivSubtype'.symm a = { carrier := ↑a, is_irreducible' := ⋯, is_closed' := ⋯ }
<VAR>R : Type u_1<VAR>Bornology R<VAR>Add R<VAR>self : BoundedAdd R<VAR>s t : Set R<GOAL>Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)
<VAR>R : Type u_1<VAR>Bornology R<VAR>Add R<VAR>BoundedAdd R<VAR>s t : Set R<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s + t)
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>PseudoMetricSpace R<VAR>Add R<VAR>BoundedAdd R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C
<VAR>R : Type u_1<VAR>Bornology R<VAR>Sub R<VAR>self : BoundedSub R<VAR>s t : Set R<GOAL>Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)
<VAR>R : Type u_1<VAR>Bornology R<VAR>Sub R<VAR>BoundedSub R<VAR>s t : Set R<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s - t)
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>PseudoMetricSpace R<VAR>Sub R<VAR>BoundedSub R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
<VAR>R : Type u_1<VAR>PseudoMetricSpace R<VAR>Sub R<VAR>K : ℝ≥0<VAR>lip : LipschitzWith K fun p => p.1 - p.2<GOAL>BoundedSub R
<VAR>R : Type u_1<VAR>Bornology R<VAR>Mul R<VAR>self : BoundedMul R<VAR>s t : Set R<GOAL>Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)
<VAR>R : Type u_1<VAR>Bornology R<VAR>Mul R<VAR>BoundedMul R<VAR>s t : Set R<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s * t)
<VAR>R : Type u_2<VAR>Bornology R<VAR>Monoid R<VAR>BoundedMul R<VAR>s : Set R<VAR>s_bdd : Bornology.IsBounded s<VAR>n : ℕ<GOAL>Bornology.IsBounded ((fun x => x ^ n) '' s)
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>PseudoMetricSpace R<VAR>Mul R<VAR>BoundedMul R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
<VAR>R : Type u_1<VAR>SeminormedAddCommGroup R<GOAL>LipschitzWith 2 fun p => p.1 - p.2
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.Compacts α<GOAL>IsCompact self.carrier
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Compacts α<GOAL>IsCompact ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Compacts α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsCompact s<GOAL>↑{ carrier := s, isCompact' := h } = s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Compacts α<GOAL>s.carrier = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Compacts α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>s t : TopologicalSpace.Compacts α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>CompactSpace α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>↑⊥ = ∅
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → TopologicalSpace.Compacts α<GOAL>↑(s.sup f) = s.sup fun i => ↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Continuous f<VAR>s : TopologicalSpace.Compacts α<GOAL>↑(TopologicalSpace.Compacts.map f hf s) = f '' ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>K : TopologicalSpace.Compacts α<GOAL>TopologicalSpace.Compacts.map id ⋯ K = K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>K : TopologicalSpace.Compacts α<GOAL>TopologicalSpace.Compacts.map (f ∘ g) ⋯ K = TopologicalSpace.Compacts.map f hf (TopologicalSpace.Compacts.map g hg K)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<VAR>K : TopologicalSpace.Compacts β<GOAL>(TopologicalSpace.Compacts.equiv f).symm K = TopologicalSpace.Compacts.map ⇑f.symm ⋯ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<VAR>K : TopologicalSpace.Compacts α<GOAL>(TopologicalSpace.Compacts.equiv f) K = TopologicalSpace.Compacts.map ⇑f ⋯ K
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>TopologicalSpace.Compacts.equiv (Homeomorph.refl α) = Equiv.refl (TopologicalSpace.Compacts α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α ≃ₜ β<VAR>g : β ≃ₜ γ<GOAL>TopologicalSpace.Compacts.equiv (f.trans g) = (TopologicalSpace.Compacts.equiv f).trans (TopologicalSpace.Compacts.equiv g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>TopologicalSpace.Compacts.equiv f.symm = (TopologicalSpace.Compacts.equiv f).symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<VAR>K : TopologicalSpace.Compacts α<GOAL>↑((TopologicalSpace.Compacts.equiv f) K) = ⇑f.symm ⁻¹' ↑K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>K : TopologicalSpace.Compacts α<VAR>L : TopologicalSpace.Compacts β<GOAL>↑(K.prod L) = ↑K ×ˢ ↑L
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.NonemptyCompacts α<GOAL>self.carrier.Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.NonemptyCompacts α<GOAL>IsCompact ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.NonemptyCompacts α<GOAL>(↑s).Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.NonemptyCompacts α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Compacts α<VAR>h : s.carrier.Nonempty<GOAL>↑{ toCompacts := s, nonempty' := h } = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.NonemptyCompacts α<GOAL>s.carrier = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.NonemptyCompacts α<GOAL>↑s.toCompacts = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.NonemptyCompacts α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>Nonempty α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>K : TopologicalSpace.NonemptyCompacts α<VAR>L : TopologicalSpace.NonemptyCompacts β<GOAL>↑(K.prod L) = ↑K ×ˢ ↑L
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.PositiveCompacts α<GOAL>(interior self.carrier).Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.PositiveCompacts α<GOAL>IsCompact ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.PositiveCompacts α<GOAL>(interior ↑s).Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.PositiveCompacts α<GOAL>(↑s).Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.PositiveCompacts α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Compacts α<VAR>h : (interior s.carrier).Nonempty<GOAL>↑{ toCompacts := s, interior_nonempty' := h } = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.PositiveCompacts α<GOAL>s.carrier = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.PositiveCompacts α<GOAL>↑s.toCompacts = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.PositiveCompacts α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Continuous f<VAR>hf' : IsOpenMap f<VAR>s : TopologicalSpace.PositiveCompacts α<GOAL>↑(TopologicalSpace.PositiveCompacts.map f hf hf' s) = f '' ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>K : TopologicalSpace.PositiveCompacts α<GOAL>TopologicalSpace.PositiveCompacts.map id ⋯ ⋯ K = K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hf' : IsOpenMap f<VAR>hg' : IsOpenMap g<VAR>K : TopologicalSpace.PositiveCompacts α<GOAL>TopologicalSpace.PositiveCompacts.map (f ∘ g) ⋯ ⋯ K = TopologicalSpace.PositiveCompacts.map f hf hf' (TopologicalSpace.PositiveCompacts.map g hg hg' K)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LocallyCompactSpace α<VAR>U : Set α<VAR>ho : IsOpen U<VAR>hn : U.Nonempty<GOAL>∃ K, ↑K ⊆ U
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R1Space α<VAR>LocallyCompactSpace α<VAR>U : Set α<VAR>ho : IsOpen U<VAR>hn : U.Nonempty<GOAL>∃ K, closure ↑K ⊆ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>K : TopologicalSpace.PositiveCompacts α<VAR>L : TopologicalSpace.PositiveCompacts β<GOAL>↑(K.prod L) = ↑K ×ˢ ↑L
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.CompactOpens α<GOAL>IsOpen self.carrier
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.CompactOpens α<GOAL>IsCompact ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.CompactOpens α<GOAL>IsOpen ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.CompactOpens α<GOAL>↑s.toOpens = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>s : TopologicalSpace.CompactOpens α<GOAL>↑s.toClopens = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.CompactOpens α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Compacts α<VAR>h : IsOpen s.carrier<GOAL>↑{ toCompacts := s, isOpen' := h } = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.CompactOpens α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>QuasiSeparatedSpace α<VAR>s t : TopologicalSpace.CompactOpens α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>s t : TopologicalSpace.CompactOpens α<GOAL>↑(s \ t) = ↑s \ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>T2Space α<VAR>s : TopologicalSpace.CompactOpens α<GOAL>↑sᶜ = (↑s)ᶜ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>T2Space α<VAR>s t : TopologicalSpace.CompactOpens α<GOAL>↑(s ⇨ t) = ↑s ⇨ ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Continuous f<VAR>hf' : IsOpenMap f<VAR>s : TopologicalSpace.CompactOpens α<GOAL>(TopologicalSpace.CompactOpens.map f hf hf' s).toCompacts = TopologicalSpace.Compacts.map f hf s.toCompacts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Continuous f<VAR>hf' : IsOpenMap f<VAR>s : TopologicalSpace.CompactOpens α<GOAL>↑(TopologicalSpace.CompactOpens.map f hf hf' s) = f '' ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>K : TopologicalSpace.CompactOpens α<GOAL>TopologicalSpace.CompactOpens.map id ⋯ ⋯ K = K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hf' : IsOpenMap f<VAR>hg' : IsOpenMap g<VAR>K : TopologicalSpace.CompactOpens α<GOAL>TopologicalSpace.CompactOpens.map (f ∘ g) ⋯ ⋯ K = TopologicalSpace.CompactOpens.map f hf hf' (TopologicalSpace.CompactOpens.map g hg hg' K)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>K : TopologicalSpace.CompactOpens α<VAR>L : TopologicalSpace.CompactOpens β<GOAL>↑(K.prod L) = ↑K ×ˢ ↑L
<VAR>X : Type u<VAR>s : Set X<VAR>p : Set X → Prop<VAR>h₁ : p Set.univ<VAR>h₂ : ∀ (s t : Set X), p s → p t → p (s ∩ t)<VAR>h₃ : ∀ (s : Set (Set X)), (∀ t ∈ s, p t) → p (⋃₀ s)<GOAL>IsOpen s ↔ p s
<VAR>X : Type u<VAR>f g : TopologicalSpace X<GOAL>IsOpen = IsOpen → f = g
<VAR>X : Type u<VAR>t t' : TopologicalSpace X<GOAL>t = t' ↔ ∀ (s : Set X), IsOpen s ↔ IsOpen s
<VAR>X : Type u<VAR>s : Set X<VAR>t : TopologicalSpace X<GOAL>TopologicalSpace.IsOpen s = IsOpen s
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (f i)<GOAL>IsOpen (⋃ i, f i)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>s : Set α<VAR>f : α → Set X<VAR>h : ∀ i ∈ s, IsOpen (f i)<GOAL>IsOpen (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>s₁ s₂ : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsOpen s₁<VAR>h₂ : IsOpen s₂<GOAL>IsOpen (s₁ ∪ s₂)
<VAR>X : Type u<VAR>α : Type u_1<VAR>s : Set X<VAR>TopologicalSpace X<VAR>f : α → Set X<VAR>ho : ∀ (i : α), IsOpen (f i)<VAR>hU : ⋃ i, f i = Set.univ<GOAL>IsOpen s ↔ ∀ (i : α), IsOpen (f i ∩ s)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpen ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set (Set X)<VAR>hs : s.Finite<GOAL>(∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>s : Set α<VAR>f : α → Set X<VAR>hs : s.Finite<VAR>h : ∀ i ∈ s, IsOpen (f i)<GOAL>IsOpen (⋂ i ∈ s, f i)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>Finite ι<VAR>s : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (s i)<GOAL>IsOpen (⋂ i, s i)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>s : Finset α<VAR>f : α → Set X<VAR>h : ∀ i ∈ s, IsOpen (f i)<GOAL>IsOpen (⋂ i ∈ s, f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : Prop<GOAL>IsOpen {_x | p}
<VAR>X : Type u<VAR>p₁ p₂ : X → Prop<VAR>TopologicalSpace X<GOAL>IsOpen {x | p₁ x} → IsOpen {x | p₂ x} → IsOpen {x | p₁ x ∧ p₂ x}
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen sᶜ ↔ IsClosed s
<VAR>X : Type u<VAR>t₁ t₂ : TopologicalSpace X<GOAL>t₁ = t₂ ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : Prop<GOAL>IsClosed {_x | p}
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosed ∅
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosed Set.univ
<VAR>X : Type u<VAR>s₁ s₂ : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set (Set X)<GOAL>(∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>h : ∀ (i : ι), IsClosed (f i)<GOAL>IsClosed (⋂ i, f i)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>s : Set α<VAR>f : α → Set X<VAR>h : ∀ i ∈ s, IsClosed (f i)<GOAL>IsClosed (⋂ i ∈ s, f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsClosed sᶜ ↔ IsOpen s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsOpen s<VAR>h₂ : IsClosed t<GOAL>IsOpen (s \ t)
<VAR>X : Type u<VAR>s₁ s₂ : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsClosed s₁<VAR>h₂ : IsClosed s₂<GOAL>IsClosed (s₁ ∩ s₂)
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsClosed s<VAR>h₂ : IsOpen t<GOAL>IsClosed (s \ t)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>s : Set α<VAR>f : α → Set X<VAR>hs : s.Finite<VAR>h : ∀ i ∈ s, IsClosed (f i)<GOAL>IsClosed (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>s : Finset α<VAR>f : α → Set X<VAR>h : ∀ i ∈ s, IsClosed (f i)<GOAL>IsClosed (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>Finite ι<VAR>s : ι → Set X<VAR>h : ∀ (i : ι), IsClosed (s i)<GOAL>IsClosed (⋃ i, s i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p q : X → Prop<VAR>hp : IsOpen {x | p x}<VAR>hq : IsClosed {x | q x}<GOAL>IsClosed {x | p x → q x}
<VAR>X : Type u<VAR>p : X → Prop<VAR>TopologicalSpace X<GOAL>IsClosed {a | p a} → IsOpen {a | ¬p a}
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen (interior s)
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s ⊆ s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : t ⊆ s<VAR>h₂ : IsOpen t<GOAL>t ⊆ interior s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : IsOpen s<GOAL>interior s = s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s = s ↔ IsOpen s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>s ⊆ interior s ↔ IsOpen s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsOpen s<GOAL>s ⊆ interior t ↔ s ⊆ t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h : s ⊆ t<GOAL>interior s ⊆ interior t
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>interior ∅ = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>interior Set.univ = Set.univ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s = Set.univ ↔ s = Set.univ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior (interior s) = interior s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>interior (s ∩ t) = interior s ∩ interior t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set X<GOAL>interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : S.Finite<GOAL>interior (⋂₀ S) = ⋂ s ∈ S, interior s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → Set X<GOAL>interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>Finite ι<VAR>f : ι → Set X<GOAL>interior (⋂ i, f i) = ⋂ i, interior (f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>f : ℕ → Set X<GOAL>interior (⋂ m, ⋂ (_ : m < n), f m) = ⋂ m, ⋂ (_ : m < n), interior (f m)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>f : ℕ → Set X<GOAL>interior (⋂ m, ⋂ (_ : m ≤ n), f m) = ⋂ m, ⋂ (_ : m ≤ n), interior (f m)
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsClosed s<VAR>h₂ : interior t = ∅<GOAL>interior (s ∪ t) = interior s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>s : ι → Set X<GOAL>interior (⋂ i, s i) ⊆ ⋂ i, interior (s i)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>p : ι → Sort u_3<VAR>s : (i : ι) → p i → Set X<GOAL>interior (⋂ i, ⋂ j, s i j) ⊆ ⋂ i, ⋂ j, interior (s i j)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<GOAL>interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>l : Filter X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : l.HasBasis p s<GOAL>(l.lift' interior).HasBasis p fun i => interior (s i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>l : Filter X<GOAL>l.lift' interior ≤ l
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>l : Filter X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : l.HasBasis p s<VAR>ho : ∀ (i : ι), p i → IsOpen (s i)<GOAL>l.lift' interior = l
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed (closure s)
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>s ⊆ closure s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>P : X<VAR>hP : P ∉ closure s<GOAL>P ∉ s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : s ⊆ t<VAR>h₂ : IsClosed t<GOAL>closure s ⊆ t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hd : Disjoint s t<VAR>ht : IsOpen t<GOAL>Disjoint (closure s) t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hd : Disjoint s t<VAR>hs : IsOpen s<GOAL>Disjoint s (closure t)
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : IsClosed s<GOAL>closure s = s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsClosed s<GOAL>closure s ⊆ s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h₁ : IsClosed t<GOAL>closure s ⊆ t ↔ s ⊆ t
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsClosed s<GOAL>x ∈ s ↔ closure {x} ⊆ s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h : s ⊆ t<GOAL>closure s ⊆ closure t
<VAR>X : Type u_3<VAR>TopologicalSpace X<GOAL>Monotone closure
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>s \ t ⊆ closure t ↔ s ⊆ closure t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>closure (s ∩ t) ⊆ closure s ∩ closure t
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : closure s ⊆ s<GOAL>IsClosed s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>closure s = s ↔ IsClosed s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>closure s ⊆ s ↔ IsClosed s
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>closure ∅ = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>closure s = ∅ ↔ s = ∅
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>(closure s).Nonempty ↔ s.Nonempty
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>closure Set.univ = Set.univ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>closure (closure s) = closure s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>closure s = (interior sᶜ)ᶜ
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>closure (s ∪ t) = closure s ∪ closure t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set X<GOAL>closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)