ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>g = CategoryTheory.CategoryStruct.comp α.inv f ↔ CategoryTheory.CategoryStruct.comp α.hom g = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : Z ⟶ Y<VAR>g : Z ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp f α.inv = g ↔ f = CategoryTheory.CategoryStruct.comp g α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : Z ⟶ Y<VAR>g : Z ⟶ X<GOAL>g = CategoryTheory.CategoryStruct.comp f α.inv ↔ CategoryTheory.CategoryStruct.comp g α.hom = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ≅ Y<GOAL>f.inv = g.inv ↔ f.hom = g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : Y ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp α.hom f = CategoryTheory.CategoryStruct.id X ↔ f = α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : Y ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp f α.hom = CategoryTheory.CategoryStruct.id Y ↔ f = α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp α.inv f = CategoryTheory.CategoryStruct.id Y ↔ f = α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f α.inv = CategoryTheory.CategoryStruct.id X ↔ f = α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>β : Y ≅ X<GOAL>α.hom = β.inv ↔ β.hom = α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>α.homToEquiv.symm g = CategoryTheory.CategoryStruct.comp g α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>f : Z ⟶ X<GOAL>α.homToEquiv f = CategoryTheory.CategoryStruct.comp f α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>g : Y ⟶ Z<GOAL>α.homFromEquiv.symm g = CategoryTheory.CategoryStruct.comp α.hom g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>f : X ⟶ Z<GOAL>α.homFromEquiv f = CategoryTheory.CategoryStruct.comp α.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.IsIso f<GOAL>∃ inv, CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.IsIso f<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.IsIso f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) f = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.IsIso f<VAR>Z : C<VAR>g : X ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g) = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.IsIso f<VAR>Z : C<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp f g) = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>CategoryTheory.IsIso e.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>CategoryTheory.IsIso e.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ {x : CategoryTheory.IsIso f}, (CategoryTheory.asIso f).hom = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ {x : CategoryTheory.IsIso f}, (CategoryTheory.asIso f).inv = CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>g : Y ⟶ X<VAR>hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X<GOAL>CategoryTheory.inv f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>g : Y ⟶ X<VAR>inv_hom_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y<GOAL>CategoryTheory.inv f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>g : Y ⟶ X<VAR>hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X<GOAL>g = CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>g : Y ⟶ X<VAR>inv_hom_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y<GOAL>g = CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>CategoryTheory.inv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.IsIso h<GOAL>CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) (CategoryTheory.inv f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.inv (CategoryTheory.inv f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ≅ Y<GOAL>CategoryTheory.inv f.inv = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ≅ Y<GOAL>CategoryTheory.inv f.hom = f.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ⟶ Y<VAR>CategoryTheory.IsIso α<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f = g ↔ f = CategoryTheory.CategoryStruct.comp α g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ⟶ Y<VAR>CategoryTheory.IsIso α<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f ↔ CategoryTheory.CategoryStruct.comp α g = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ⟶ Y<VAR>CategoryTheory.IsIso α<VAR>f : Z ⟶ Y<VAR>g : Z ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) = g ↔ f = CategoryTheory.CategoryStruct.comp g α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ⟶ Y<VAR>CategoryTheory.IsIso α<VAR>f : Z ⟶ Y<VAR>g : Z ⟶ X<GOAL>g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) ↔ CategoryTheory.CategoryStruct.comp g α = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)<GOAL>CategoryTheory.IsIso g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<VAR>CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : X ⟶ Z<VAR>CategoryTheory.IsIso f<VAR>hh : CategoryTheory.IsIso h<VAR>w : CategoryTheory.CategoryStruct.comp f g = h<GOAL>CategoryTheory.IsIso g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : X ⟶ Z<VAR>CategoryTheory.IsIso g<VAR>hh : CategoryTheory.IsIso h<VAR>w : CategoryTheory.CategoryStruct.comp f g = h<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.IsIso g<VAR>p : CategoryTheory.inv f = CategoryTheory.inv g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.IsIso g<GOAL>CategoryTheory.inv f = CategoryTheory.inv g ↔ f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>CategoryTheory.IsIso g<VAR>f : Y ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>CategoryTheory.IsIso g<VAR>f : Y ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id Y ↔ f = CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>CategoryTheory.IsIso g<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f = CategoryTheory.CategoryStruct.id Y ↔ f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>CategoryTheory.IsIso g<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g) = CategoryTheory.CategoryStruct.id X ↔ f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>CategoryTheory.IsIso g<VAR>f : Y ⟶ X<VAR>h : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>CategoryTheory.IsIso g<VAR>f : Y ⟶ X<VAR>h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id Y<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>g : Y ⟶ X<VAR>hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X<GOAL>f.inv = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>g : Y ⟶ X<VAR>hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X<GOAL>g = f.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ≅ Y<VAR>g g' : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.comp f.hom g' ↔ g = g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : Y ≅ X<VAR>g g' : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f.inv g = CategoryTheory.CategoryStruct.comp f.inv g' ↔ g = g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f f' : X ⟶ Y<VAR>g : Y ≅ Z<GOAL>CategoryTheory.CategoryStruct.comp f g.hom = CategoryTheory.CategoryStruct.comp f' g.hom ↔ f = f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f f' : X ⟶ Y<VAR>g : Z ≅ Y<GOAL>CategoryTheory.CategoryStruct.comp f g.inv = CategoryTheory.CategoryStruct.comp f' g.inv ↔ f = f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X X' Y Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y<VAR>h : Y ≅ Z<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.hom) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.hom) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X X' Y Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y<VAR>h : Z ≅ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.inv) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.inv) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C D<GOAL>CategoryTheory.CategoryStruct.comp (F.map e.hom) (F.map e.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C D<GOAL>CategoryTheory.CategoryStruct.comp (F.map e.inv) (F.map e.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>i : X ≅ Y<GOAL>(F.mapIso i).inv = F.map i.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>i : X ≅ Y<GOAL>(F.mapIso i).hom = F.map i.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>i : X ≅ Y<GOAL>F.mapIso i.symm = (F.mapIso i).symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y Z : C<VAR>i : X ≅ Y<VAR>j : Y ≅ Z<GOAL>F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>F.mapIso (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>F.map (CategoryTheory.inv f) = CategoryTheory.inv (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (F.map f) = CategoryTheory.CategoryStruct.id (F.obj Y)
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>self : MeasureTheory.Conservative f μ<VAR>s : Set α<GOAL>MeasurableSet s → μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : MeasureTheory.MeasurePreserving f μ μ<GOAL>MeasureTheory.Conservative f μ
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Conservative id μ
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hsm : MeasureTheory.NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<GOAL>∃ᶠ (m : ℕ) in Filter.atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>N : ℕ<GOAL>∃ m > N, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>n : ℕ<GOAL>μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>s ∩ {x | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s} =ᵐ[μ] s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>μ (s ∩ {x | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s}) = μ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<GOAL>∃ᵐ (x : α) ∂μ, x ∈ s ∧ ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>OpensMeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.Conservative f μ<GOAL>∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.Conservative f μ<VAR>n : ℕ<GOAL>MeasureTheory.Conservative f^[n] μ
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<GOAL>omegaLimit f ϕ s = ⋂ u ∈ f, closure (Set.image2 ϕ u s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>m : τ → τ<VAR>f₁ f₂ : Filter τ<VAR>hf : Filter.Tendsto m f₁ f₂<GOAL>omegaLimit f₁ (fun t x => ϕ (m t) x) s ⊆ omegaLimit f₂ ϕ s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>f₁ f₂ : Filter τ<VAR>hf : f₁ ≤ f₂<GOAL>omegaLimit f₁ ϕ s ⊆ omegaLimit f₂ ϕ s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s₁ s₂ : Set α<VAR>hs : s₁ ⊆ s₂<GOAL>omegaLimit f ϕ s₁ ⊆ omegaLimit f ϕ s₂
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<GOAL>IsClosed (omegaLimit f ϕ s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>s : Set α<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>TopologicalSpace β'<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>ϕ' : τ → α' → β'<VAR>ga : α → α'<VAR>s' : Set α'<VAR>hs : Set.MapsTo ga s s'<VAR>gb : β → β'<VAR>hg : ∀ᶠ (t : τ) in f, Set.EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s<VAR>hgc : Continuous gb<GOAL>Set.MapsTo gb (omegaLimit f ϕ s) (omegaLimit f ϕ' s')
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>s : Set α<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>TopologicalSpace β'<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>ϕ' : τ → α' → β'<VAR>ga : α → α'<VAR>s' : Set α'<VAR>hs : Set.MapsTo ga s s'<VAR>gb : β → β'<VAR>hg : ∀ (t : τ) (x : α), gb (ϕ t x) = ϕ' t (ga x)<VAR>hgc : Continuous gb<GOAL>Set.MapsTo gb (omegaLimit f ϕ s) (omegaLimit f ϕ' s')
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>s : Set α<VAR>α' : Type u_5<VAR>ϕ : τ → α' → β<VAR>f : Filter τ<VAR>g : α → α'<GOAL>omegaLimit f ϕ (g '' s) = omegaLimit f (fun t x => ϕ t (g x)) s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>α' : Type u_5<VAR>ϕ : τ → α' → β<VAR>s : Set α'<VAR>f : Filter τ<VAR>g : α → α'<GOAL>omegaLimit f (fun t x => ϕ t (g x)) (g ⁻¹' s) ⊆ omegaLimit f ϕ s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>y : β<GOAL>y ∈ omegaLimit f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>y : β<GOAL>y ∈ omegaLimit f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>x : α<VAR>y : β<GOAL>y ∈ omegaLimit f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s₁ s₂ : Set α<GOAL>omegaLimit f ϕ (s₁ ∩ s₂) ⊆ omegaLimit f ϕ s₁ ∩ omegaLimit f ϕ s₂
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>p : ι → Set α<GOAL>omegaLimit f ϕ (⋂ i, p i) ⊆ ⋂ i, omegaLimit f ϕ (p i)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s₁ s₂ : Set α<GOAL>omegaLimit f ϕ (s₁ ∪ s₂) = omegaLimit f ϕ s₁ ∪ omegaLimit f ϕ s₂
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>p : ι → Set α<GOAL>⋃ i, omegaLimit f ϕ (p i) ⊆ omegaLimit f ϕ (⋃ i, p i)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<GOAL>omegaLimit f ϕ s = ⋂ u, closure (Set.image2 ϕ (↑u) s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>v : Set τ<VAR>hv : v ∈ f<GOAL>omegaLimit f ϕ s = ⋂ u ∈ f, closure (Set.image2 ϕ (u ∩ v) s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>v : Set τ<VAR>hv : v ∈ f<GOAL>omegaLimit f ϕ s = ⋂ u, closure (Set.image2 ϕ (↑u ∩ v) s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>u : Set τ<VAR>hu : u ∈ f<GOAL>omegaLimit f ϕ s ⊆ closure (Set.image2 ϕ u s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : omegaLimit f ϕ s ⊆ n<GOAL>∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>T2Space β<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : omegaLimit f ϕ s ⊆ n<GOAL>∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>T2Space β<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : omegaLimit f ϕ s ⊆ n<GOAL>∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>CompactSpace β<VAR>v : Set β<VAR>hv₁ : IsOpen v<VAR>hv₂ : omegaLimit f ϕ s ⊆ v<GOAL>∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ v
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>CompactSpace β<VAR>v : Set β<VAR>hv₁ : IsOpen v<VAR>hv₂ : omegaLimit f ϕ s ⊆ v<GOAL>∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s v
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c<VAR>hs : s.Nonempty<GOAL>(omegaLimit f ϕ s).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s : Set α<VAR>CompactSpace β<VAR>f.NeBot<VAR>hs : s.Nonempty<GOAL>(omegaLimit f ϕ s).Nonempty
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddMonoid τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Filter.Tendsto (fun x => t + x) f f<GOAL>IsInvariant ϕ.toFun (omegaLimit f ϕ.toFun s)
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddMonoid τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>t : τ<VAR>ht : Filter.Tendsto (fun x => x + t) f f<GOAL>omegaLimit f ϕ.toFun (ϕ.toFun t '' s) ⊆ omegaLimit f ϕ.toFun s