ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>L : Type u_4<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Field L<VAR>algRL : Algebra R L<VAR>Algebra R S<VAR>Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<VAR>IsDedekindDomain S<VAR>Algebra.IsAlgebraic R L<GOAL>Function.Surjective (ClassGroup.mkMMem bS adm)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : TopologicalSpace.Compacts X<GOAL>(⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}).Nonempty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K₁ K₂ : TopologicalSpace.Compacts X<VAR>h : K₁ ≤ K₂<GOAL>rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : TopologicalSpace.Compacts X<VAR>f : X →ᵇ ℝ≥0<VAR>h : ∀ x ∈ K, 1 ≤ f x<GOAL>rieszContentAux Λ K ≤ Λ f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : TopologicalSpace.Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : TopologicalSpace.Compacts X<GOAL>rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>l.IsMeasurablyGenerated<VAR>hf : f =O[l] g<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hg : MeasureTheory.IntegrableAtFilter g l μ<GOAL>MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : f =O[⊤] g<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>(Filter.cocompact α).IsMeasurablyGenerated<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>ho : f =O[Filter.cocompact α] g<VAR>hg : MeasureTheory.IntegrableAtFilter g (Filter.cocompact α) μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>CompactIccSpace α<VAR>g' : α → F<VAR>Filter.atBot.IsMeasurablyGenerated<VAR>Filter.atTop.IsMeasurablyGenerated<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>ho : f =O[Filter.atBot] g<VAR>hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ<VAR>ho' : f =O[Filter.atTop] g'<VAR>hg' : MeasureTheory.IntegrableAtFilter g' Filter.atTop μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a : α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>CompactIccSpace α<VAR>Filter.atBot.IsMeasurablyGenerated<VAR>hf : MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ<VAR>ho : f =O[Filter.atBot] g<VAR>hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ<GOAL>MeasureTheory.IntegrableOn f (Set.Iic a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a : α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>CompactIccSpace α<VAR>Filter.atTop.IsMeasurablyGenerated<VAR>hf : MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ<VAR>ho : f =O[Filter.atTop] g<VAR>hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ<GOAL>MeasureTheory.IntegrableOn f (Set.Ici a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>CompactIccSpace α<VAR>Filter.atBot.IsMeasurablyGenerated<VAR>OrderTop α<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>ho : f =O[Filter.atBot] g<VAR>hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>CompactIccSpace α<VAR>Filter.atTop.IsMeasurablyGenerated<VAR>OrderBot α<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>ho : f =O[Filter.atTop] g<VAR>hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrderedAddCommGroup α<VAR>CompactIccSpace α<VAR>Filter.atTop.IsMeasurablyGenerated<VAR>MeasurableNeg α<VAR>μ.IsNegInvariant<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[Filter.atTop] g<VAR>hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ<GOAL>MeasureTheory.Integrable f μ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>M : Type w<VAR>Nonempty M<VAR>L.Structure M<VAR>M ⊨ T<GOAL>T.IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T T' : L.Theory<VAR>h : T'.IsSatisfiable<VAR>hs : T ⊆ T'<GOAL>T.IsSatisfiable
<VAR>L : FirstOrder.Language<GOAL>∅.IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>L' : FirstOrder.Language<VAR>φ : L →ᴸ L'<VAR>h : (φ.onTheory T).IsSatisfiable<GOAL>T.IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>L' : FirstOrder.Language<VAR>φ : L →ᴸ L'<VAR>h : φ.Injective<GOAL>(φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsSatisfiable<GOAL>T.IsFinitelySatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<GOAL>T.IsSatisfiable ↔ T.IsFinitelySatisfiable
<VAR>L : FirstOrder.Language<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>T : ι → L.Theory<VAR>h : Directed (fun x x_1 => x ⊆ x_1) T<GOAL>FirstOrder.Language.Theory.IsSatisfiable (⋃ i, T i) ↔ ∀ (i : ι), (T i).IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>α : Type w<VAR>T : L.Theory<VAR>s : Set α<VAR>M : Type w'<VAR>Nonempty M<VAR>L.Structure M<VAR>M ⊨ T<VAR>h : Cardinal.lift.{w', w} #↑s ≤ Cardinal.lift.{w, w'} #M<GOAL>((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>α : Type w<VAR>T : L.Theory<VAR>s : Set α<VAR>M : Type w'<VAR>L.Structure M<VAR>M ⊨ T<VAR>Infinite M<GOAL>((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>L.Structure M<VAR>M ⊨ T<VAR>Infinite M<GOAL>∃ N, Cardinal.lift.{max u v w, w} κ ≤ #↑N
<VAR>L : FirstOrder.Language<VAR>ι : Type u_1<VAR>T : ι → L.Theory<GOAL>FirstOrder.Language.Theory.IsSatisfiable (⋃ i, T i) ↔ ∀ (s : Finset ι), FirstOrder.Language.Theory.IsSatisfiable (⋃ i ∈ s, T i)
<VAR>L : FirstOrder.Language<VAR>M : Type w'<VAR>L.Structure M<VAR>Nonempty M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ<VAR>h3 : Cardinal.lift.{w', w} κ ≤ Cardinal.lift.{w, w'} #M<GOAL>∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
<VAR>L : FirstOrder.Language<VAR>M : Type w'<VAR>L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ<VAR>h2 : Cardinal.lift.{w, w'} #M ≤ Cardinal.lift.{w', w} κ<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>L : FirstOrder.Language<VAR>M : Type w'<VAR>L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ<GOAL>∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
<VAR>L : FirstOrder.Language<VAR>M : Type w'<VAR>L.Structure M<VAR>Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ<GOAL>∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : ∃ M, Infinite ↑M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ<GOAL>∃ N, #↑N = κ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ : L.Formula α<GOAL>T ⊨ᵇ φ ↔ ∀ (M : T.ModelType) (v : α → ↑M), φ.Realize v
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ φ ↔ ∀ (M : T.ModelType), ↑M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>φ : L.Sentence<VAR>h : φ ∈ T<GOAL>T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ φ ↔ ¬(T ∪ {FirstOrder.Language.Formula.not φ}).IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>φ : L.Sentence<VAR>h : T ⊨ᵇ φ<VAR>M : Type u_1<VAR>L.Structure M<VAR>M ⊨ T<VAR>Nonempty M<GOAL>M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>T' : L.Theory<VAR>h : ∀ φ ∈ T', T ⊨ᵇ φ<VAR>φ : L.Formula α<VAR>hφ : T' ⊨ᵇ φ<GOAL>T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsComplete<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ FirstOrder.Language.Formula.not φ ↔ ¬T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsComplete<VAR>φ : L.Sentence<VAR>M : Type u_1<VAR>L.Structure M<VAR>M ⊨ T<VAR>Nonempty M<GOAL>M ⊨ φ ↔ T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsMaximal<GOAL>T.IsComplete
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsMaximal<VAR>φ : L.Sentence<GOAL>φ ∈ T ∨ FirstOrder.Language.Formula.not φ ∈ T
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsMaximal<VAR>φ : L.Sentence<VAR>hφ : T ⊨ᵇ φ<GOAL>φ ∈ T
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>h : T.IsMaximal<VAR>φ : L.Sentence<GOAL>φ ∈ T ↔ T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>T.SemanticallyEquivalent φ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent ψ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ θ : L.BoundedFormula α n<VAR>h1 : T.SemanticallyEquivalent φ ψ<VAR>h2 : T.SemanticallyEquivalent ψ θ<GOAL>T.SemanticallyEquivalent φ θ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>M : Type (max u v)<VAR>Nonempty M<VAR>L.Structure M<VAR>M ⊨ T<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>φ.Realize v xs ↔ ψ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ ψ : L.Formula α<VAR>M : Type (max u v)<VAR>Nonempty M<VAR>L.Structure M<VAR>_hM : M ⊨ T<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>v : α → M<GOAL>φ.Realize v ↔ ψ.Realize v
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α (n + 1)<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent (∀'φ) (∀'ψ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α (n + 1)<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent (∃'φ) (∃'ψ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent (∼φ) ∼ψ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ φ' ψ' : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>h' : T.SemanticallyEquivalent φ' ψ'<GOAL>T.SemanticallyEquivalent (φ ⟹ φ') (ψ ⟹ ψ')
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>Nonempty M<GOAL>(L.completeTheory M).IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>φ : L.Sentence<GOAL>φ ∈ L.completeTheory M ∨ FirstOrder.Language.Formula.not φ ∈ L.completeTheory M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>Nonempty M<GOAL>(L.completeTheory M).IsMaximal
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>Nonempty M<GOAL>(L.completeTheory M).IsComplete
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>T.SemanticallyEquivalent φ ∼∼φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>T.SemanticallyEquivalent (φ ⟹ ψ) (∼φ ⊔ ψ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>T.SemanticallyEquivalent (φ ⊔ ψ) ∼(∼φ ⊓ ∼ψ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>T.SemanticallyEquivalent (φ ⊓ ψ) ∼(∼φ ⊔ ∼ψ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>T.SemanticallyEquivalent (∀'φ) ∼(∃'∼φ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>T.SemanticallyEquivalent (∃'φ) ∼(∀'∼φ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>T.SemanticallyEquivalent φ (∀'FirstOrder.Language.BoundedFormula.liftAt 1 n φ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ : L.Formula α<GOAL>T.SemanticallyEquivalent φ φ.not.not
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ ψ : L.Formula α<GOAL>T.SemanticallyEquivalent (φ.imp ψ) (φ.not ⊔ ψ)
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ ψ : L.Formula α<GOAL>T.SemanticallyEquivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ ψ : L.Formula α<GOAL>T.SemanticallyEquivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not
<VAR>L : FirstOrder.Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<GOAL>T.IsComplete
<VAR>κ : Cardinal.{w}<VAR>T : FirstOrder.Language.empty.Theory<GOAL>κ.Categorical T
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s : Set (α → M)<VAR>L' : FirstOrder.Language<VAR>L'.Structure M<VAR>h : A.Definable L s<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<GOAL>A.Definable L' s
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s : Set (α → M)<GOAL>A.Definable L s ↔ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}
<VAR>M : Type w<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s : Set (α → M)<GOAL>∅.Definable L s ↔ ∃ φ, s = setOf φ.Realize
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s : Set (α → M)<GOAL>A.Definable L s ↔ ∅.Definable (L.withConstants ↑A) s
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>B : Set M<VAR>s : Set (α → M)<VAR>hAs : A.Definable L s<VAR>hAB : A ⊆ B<GOAL>B.Definable L s
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<GOAL>A.Definable L ∅
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<GOAL>A.Definable L Set.univ
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>f g : Set (α → M)<VAR>hf : A.Definable L f<VAR>hg : A.Definable L g<GOAL>A.Definable L (f ∩ g)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>f g : Set (α → M)<VAR>hf : A.Definable L f<VAR>hg : A.Definable L g<GOAL>A.Definable L (f ∪ g)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>ι : Type u_2<VAR>f : ι → Set (α → M)<VAR>hf : ∀ (i : ι), A.Definable L (f i)<VAR>s : Finset ι<GOAL>A.Definable L (s.inf f)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>ι : Type u_2<VAR>f : ι → Set (α → M)<VAR>hf : ∀ (i : ι), A.Definable L (f i)<VAR>s : Finset ι<GOAL>A.Definable L (s.sup f)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>ι : Type u_2<VAR>f : ι → Set (α → M)<VAR>hf : ∀ (i : ι), A.Definable L (f i)<VAR>s : Finset ι<GOAL>A.Definable L (⋂ i ∈ s, f i)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>ι : Type u_2<VAR>f : ι → Set (α → M)<VAR>hf : ∀ (i : ι), A.Definable L (f i)<VAR>s : Finset ι<GOAL>A.Definable L (⋃ i ∈ s, f i)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s : Set (α → M)<VAR>hf : A.Definable L s<GOAL>A.Definable L sᶜ
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s t : Set (α → M)<VAR>hs : A.Definable L s<VAR>ht : A.Definable L t<GOAL>A.Definable L (s \ t)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s t : Set (α → M)<VAR>hs : A.Definable L s<VAR>ht : A.Definable L t<GOAL>A.Definable L (s ⇨ t)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>f : α → β<VAR>s : Set (α → M)<VAR>h : A.Definable L s<GOAL>A.Definable L ((fun g => g ∘ f) ⁻¹' s)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ≃ β<GOAL>A.Definable L ((fun g => g ∘ ⇑f) '' s)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>s : Set (α → M)<GOAL>A.Definable L s ↔ ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>m : ℕ<VAR>s : Set (α ⊕ Fin m → M)<VAR>h : A.Definable L s<GOAL>A.Definable L ((fun g => g ∘ Sum.inl) '' s)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ↪ β<VAR>Finite β<GOAL>A.Definable L ((fun g => g ∘ ⇑f) '' s)
<VAR>M : Type w<VAR>A : Set M<VAR>L : FirstOrder.Language<VAR>L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α → β<VAR>Finite α<VAR>Finite β<GOAL>A.Definable L ((fun g => g ∘ f) '' s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<GOAL>s ≤ t ↔ ↑s ≤ ↑t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>x : α → M<GOAL>x ∈ ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>x : α → M<GOAL>x ∉ ⊥
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<VAR>x : α → M<GOAL>x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<VAR>x : α → M<GOAL>x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s : L.DefinableSet A α<VAR>x : α → M<GOAL>x ∈ sᶜ ↔ x ∉ s
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<VAR>x : α → M<GOAL>x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<GOAL>↑⊤ = Set.univ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<GOAL>↑⊥ = ∅
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s : L.DefinableSet A α<GOAL>↑sᶜ = (↑s)ᶜ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<GOAL>↑(s \ t) = ↑s \ ↑t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>α : Type u₁<VAR>s t : L.DefinableSet A α<GOAL>↑(s ⇨ t) = ↑s ⇨ ↑t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<VAR>f : L.Functions n<GOAL>FirstOrder.Language.ClosedUnder f Set.univ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>s t : Set M<VAR>hs : FirstOrder.Language.ClosedUnder f s<VAR>ht : FirstOrder.Language.ClosedUnder f t<GOAL>FirstOrder.Language.ClosedUnder f (s ∩ t)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>s t : Set M<VAR>hs : FirstOrder.Language.ClosedUnder f s<VAR>ht : FirstOrder.Language.ClosedUnder f t<GOAL>FirstOrder.Language.ClosedUnder f (s ⊓ t)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>S : Set (Set M)<VAR>hS : ∀ s ∈ S, FirstOrder.Language.ClosedUnder f s<GOAL>FirstOrder.Language.ClosedUnder f (sInf S)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>self : L.Substructure M<VAR>n : ℕ<VAR>f : L.Functions n<GOAL>FirstOrder.Language.ClosedUnder f ↑self
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : L.Substructure M<VAR>x : M<GOAL>x ∈ ↑s ↔ x ∈ s
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S T : L.Substructure M<VAR>h : ∀ (x : M), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>α : Type u_3<VAR>t : L.Term α<VAR>xs : α → M<VAR>h : ∀ (a : α), xs a ∈ S<GOAL>FirstOrder.Language.Term.realize xs t ∈ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>c : L.Constants<GOAL>↑c ∈ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>↑⊤ = Set.univ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>p p' : L.Substructure M<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>p p' : L.Substructure M<VAR>x : M<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : Set (L.Substructure M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : Set (L.Substructure M)<VAR>x : M<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>ι : Sort u_3<VAR>S : ι → L.Substructure M<VAR>x : M<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>ι : Sort u_3<VAR>S : ι → L.Substructure M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ ∀ (S : L.Substructure M), s ⊆ ↑S → x ∈ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<GOAL>s ⊆ ↑((FirstOrder.Language.Substructure.closure L).toFun s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<VAR>P : M<VAR>hP : P ∉ (FirstOrder.Language.Substructure.closure L).toFun s<GOAL>P ∉ s