Fraisse

📁 Source: Mathlib/ModelTheory/Fraisse.lean

Statistics

Metric	Count
Definitions Amalgamation, Hereditary, IsFraisse, IsFraisseLimit, IsUltrahomogeneous, JointEmbedding, age	7
Theorems age_subset_age, age_eq_age, is_equiv_invariant_of_fg, amalgamation, hereditary, is_equiv_invariant, is_essentially_countable, is_nonempty, jointEmbedding, age, isExtensionPair, isFraisse, nonempty_equiv, ultrahomogeneous, age_isFraisse, amalgamation_age, extend_embedding, mem_age_of_equiv, countable_quotient, fg_substructure, has_representative_as_substructure, hereditary, is_equiv_invariant, jointEmbedding, nonempty, age_directLimit, isFraisseLimit_of_countable_infinite, isFraisse_finite, exists_cg_is_age_of, exists_countable_is_age_of_iff, isUltrahomogeneous_iff_IsExtensionPair	31
Total	38

FirstOrder.Language

Definitions

Name	Category	Theorems
Amalgamation 📖	MathDef	2 math math: IsFraisse.amalgamation, IsUltrahomogeneous.amalgamation_age
Hereditary 📖	MathDef	3 math math: exists_countable_is_age_of_iff, IsFraisse.hereditary, age.hereditary
IsFraisse 📖	CompData	4 math math: empty.isFraisse_finite, isFraisse_finite_linear_order, IsUltrahomogeneous.age_isFraisse, IsFraisseLimit.isFraisse
IsFraisseLimit 📖	CompData	2 math math: empty.isFraisseLimit_of_countable_infinite, isFraisseLimit_of_countable_nonempty_dlo
IsUltrahomogeneous 📖	MathDef	2 math math: IsFraisseLimit.ultrahomogeneous, isUltrahomogeneous_iff_IsExtensionPair
JointEmbedding 📖	MathDef	3 math math: exists_countable_is_age_of_iff, age.jointEmbedding, IsFraisse.jointEmbedding
age 📖	CompOp	16 math math: dlo_age, age.nonempty, exists_cg_is_age_of, Embedding.age_subset_age, exists_countable_is_age_of_iff, IsFraisseLimit.age, Equiv.age_eq_age, age.fg_substructure, age.countable_quotient, age.is_equiv_invariant, IsUltrahomogeneous.age_isFraisse, age.jointEmbedding, IsUltrahomogeneous.amalgamation_age, age_directLimit, age.hereditary, Structure.FG.mem_age_of_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
age_directLimit 📖	mathematical	—	age DirectLimit DirectLimit.instStructureDirectLimit Set.iUnion CategoryTheory.Bundled Structure	—	Set.ext Structure.FG.range Finset.exists_le Substructure.closure_le Finset.mem_image_of_mem Embedding.coe_toHom DirectLimit.of_apply Quotient.mk_eq_iff_out le_refl DirectLimit.equiv_iff le_rfl DirectedSystem.map_self
exists_cg_is_age_of 📖	mathematical	Set.Nonempty CategoryTheory.Bundled Structure Structure.FG CategoryTheory.Bundled.α CategoryTheory.Bundled.structure Hereditary JointEmbedding	Structure.CG age	—	Set.Countable.exists_eq_range Set.Nonempty.image Quotient.mk_out Hereditary.is_equiv_invariant_of_fg DirectedSystem.natLERec.directedSystem instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat DirectLimit.cg instCountableNat Structure.FG.cg age_directLimit subset_antisymm Set.instAntisymmSubset Set.iUnion_subset Quotient.eq_mk_iff_out Set.mem_iUnion_of_mem
exists_countable_is_age_of_iff 📖	mathematical	—	Countable CategoryTheory.Bundled.α Structure age CategoryTheory.Bundled.structure Set.Nonempty CategoryTheory.Bundled Set Set.instMembership Set.Countable equivSetoid Set.image Structure.FG Hereditary JointEmbedding	—	age.nonempty age.is_equiv_invariant age.countable_quotient age.hereditary age.jointEmbedding exists_cg_is_age_of Structure.cg_iff_countable
isUltrahomogeneous_iff_IsExtensionPair 📖	mathematical	—	IsUltrahomogeneous IsExtensionPair	—	le_sup_left IsUltrahomogeneous.extend_embedding Substructure.fg_iff_structure_fg Substructure.FG.sup Substructure.fg_closure_singleton HasSubset.Subset.trans Set.instIsTransSubset Substructure.subset_closure le_sup_right Set.mem_singleton Embedding.ext equiv_between_cg Embedding.subtype_equivRange

FirstOrder.Language.Embedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
age_subset_age 📖	mathematical	—	Set CategoryTheory.Bundled FirstOrder.Language.Structure Set.instHasSubset FirstOrder.Language.age	—	Nonempty.map

FirstOrder.Language.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
age_eq_age 📖	mathematical	—	FirstOrder.Language.age	—	le_antisymm FirstOrder.Language.Embedding.age_subset_age

FirstOrder.Language.Hereditary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_equiv_invariant_of_fg 📖	mathematical	FirstOrder.Language.Hereditary FirstOrder.Language.Structure.FG CategoryTheory.Bundled.α FirstOrder.Language.Structure CategoryTheory.Bundled.structure	CategoryTheory.Bundled Set Set.instMembership	—	FirstOrder.Language.Structure.FG.mem_age_of_equiv

FirstOrder.Language.IsFraisse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
amalgamation 📖	mathematical	—	FirstOrder.Language.Amalgamation	—	—
hereditary 📖	mathematical	—	FirstOrder.Language.Hereditary	—	—
is_equiv_invariant 📖	mathematical	—	CategoryTheory.Bundled FirstOrder.Language.Structure Set Set.instMembership	—	FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg hereditary FG
is_essentially_countable 📖	mathematical	—	Set.Countable CategoryTheory.Bundled FirstOrder.Language.Structure FirstOrder.Language.equivSetoid Set.image	—	—
is_nonempty 📖	mathematical	—	Set.Nonempty CategoryTheory.Bundled FirstOrder.Language.Structure	—	—
jointEmbedding 📖	mathematical	—	FirstOrder.Language.JointEmbedding	—	—

FirstOrder.Language.IsFraisseLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
age 📖	mathematical	FirstOrder.Language.IsFraisseLimit	FirstOrder.Language.age	—	—
isExtensionPair 📖	mathematical	FirstOrder.Language.IsFraisseLimit	FirstOrder.Language.IsExtensionPair	—	FirstOrder.Language.Substructure.FG.sup FirstOrder.Language.Substructure.fg_closure_singleton age FirstOrder.Language.Substructure.fg_iff_structure_fg le_sup_left FirstOrder.Language.IsUltrahomogeneous.extend_embedding ultrahomogeneous HasSubset.Subset.trans Set.instIsTransSubset FirstOrder.Language.Substructure.subset_closure le_sup_right Set.mem_singleton FirstOrder.Language.Embedding.ext
isFraisse 📖	mathematical	FirstOrder.Language.IsFraisseLimit	FirstOrder.Language.IsFraisse	—	age FirstOrder.Language.IsUltrahomogeneous.age_isFraisse ultrahomogeneous
nonempty_equiv 📖	mathematical	FirstOrder.Language.IsFraisseLimit	FirstOrder.Language.Equiv	—	FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.Substructure.fg_bot age FirstOrder.Language.equiv_between_cg FirstOrder.Language.Structure.cg_of_countable isExtensionPair
ultrahomogeneous 📖	mathematical	FirstOrder.Language.IsFraisseLimit	FirstOrder.Language.IsUltrahomogeneous	—	—

FirstOrder.Language.IsUltrahomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
age_isFraisse 📖	mathematical	FirstOrder.Language.IsUltrahomogeneous	FirstOrder.Language.IsFraisse FirstOrder.Language.age	—	FirstOrder.Language.age.nonempty FirstOrder.Language.age.countable_quotient FirstOrder.Language.age.hereditary FirstOrder.Language.age.jointEmbedding amalgamation_age
amalgamation_age 📖	mathematical	FirstOrder.Language.IsUltrahomogeneous	FirstOrder.Language.Amalgamation FirstOrder.Language.age	—	FirstOrder.Language.Structure.FG.range le_sup_left le_sup_right FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.Substructure.FG.sup FirstOrder.Language.Embedding.ext FirstOrder.Language.Embedding.ext_iff FirstOrder.Language.Substructure.coe_inclusion FirstOrder.Language.Equiv.symm_apply_apply FirstOrder.Language.Embedding.comp_apply FirstOrder.Language.Equiv.coe_toEmbedding FirstOrder.Language.Embedding.equivRange_apply
extend_embedding 📖	mathematical	FirstOrder.Language.IsUltrahomogeneous	FirstOrder.Language.Embedding.comp	—	FirstOrder.Language.Structure.FG.range FirstOrder.Language.Embedding.ext FirstOrder.Language.Hom.mem_range FirstOrder.Language.Embedding.embeddingLike FirstOrder.Language.Equiv.injective FirstOrder.Language.Equiv.apply_symm_apply

FirstOrder.Language.Structure.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_age_of_equiv 📖	mathematical	—	CategoryTheory.Bundled FirstOrder.Language.Structure Set Set.instMembership FirstOrder.Language.age CategoryTheory.Bundled.α CategoryTheory.Bundled.structure	—	FirstOrder.Language.Equiv.fg_iff

FirstOrder.Language.age

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_quotient 📖	mathematical	—	Set.Countable CategoryTheory.Bundled FirstOrder.Language.Structure FirstOrder.Language.equivSetoid Set.image FirstOrder.Language.age	—	Set.ext Quotient.forall FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.Substructure.fg_closure Finset.finite_toSet FirstOrder.Language.Embedding.coe_toHom Finset.coe_image FirstOrder.Language.Substructure.closure_image FirstOrder.Language.Hom.range_eq_map Set.countable_range Finset.countable
fg_substructure 📖	mathematical	FirstOrder.Language.Substructure.FG	CategoryTheory.Bundled FirstOrder.Language.Structure Set Set.instMembership FirstOrder.Language.age FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.inducedStructure	—	FirstOrder.Language.Substructure.fg_iff_structure_fg
has_representative_as_substructure 📖	mathematical	CategoryTheory.Bundled FirstOrder.Language.Structure FirstOrder.Language.equivSetoid Set Set.instMembership Set.image FirstOrder.Language.age	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.FG FirstOrder.Language.Substructure.inducedStructure	—	FirstOrder.Language.Structure.FG.range
hereditary 📖	mathematical	—	FirstOrder.Language.Hereditary FirstOrder.Language.age	—	FirstOrder.Language.Embedding.age_subset_age
is_equiv_invariant 📖	mathematical	—	CategoryTheory.Bundled FirstOrder.Language.Structure Set Set.instMembership FirstOrder.Language.age	—	FirstOrder.Language.Equiv.fg_iff Nonempty.map
jointEmbedding 📖	mathematical	—	FirstOrder.Language.JointEmbedding FirstOrder.Language.age	—	FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.Substructure.FG.sup FirstOrder.Language.Structure.FG.range le_sup_left le_sup_right
nonempty 📖	mathematical	—	Set.Nonempty CategoryTheory.Bundled FirstOrder.Language.Structure FirstOrder.Language.age	—	FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.Substructure.fg_closure Set.finite_empty

FirstOrder.Language.empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFraisseLimit_of_countable_infinite 📖	mathematical	—	FirstOrder.Language.IsFraisseLimit FirstOrder.Language.empty setOf CategoryTheory.Bundled FirstOrder.Language.Structure Finite CategoryTheory.Bundled.α FirstOrder.Language.Countable.countable_functions Encodable.countable FirstOrder.Language.Symbols Sum.encodable FirstOrder.Language.Functions FirstOrder.Language.Relations Sigma.encodable Nat.encodable IsEmpty.toEncodable FirstOrder.Language.instIsRelationalEmpty FirstOrder.Language.instIsAlgebraicEmpty	—	FirstOrder.Language.Countable.countable_functions Encodable.countable FirstOrder.Language.Substructure.FG.finite Set.Infinite.to_subtype Set.Finite.infinite_compl Set.toFinite FirstOrder.Language.Structure.FG.range FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.strongHomClassEmpty nonempty_equiv_of_countable Subtype.countable FirstOrder.Language.Embedding.ext Equiv.sumCompl_symm_apply_of_pos Subtype.coe_eta Set.ext Cardinal.lift_id Cardinal.mk_eq_aleph0 Finite.to_countable
isFraisse_finite 📖	mathematical	—	FirstOrder.Language.IsFraisse FirstOrder.Language.empty setOf CategoryTheory.Bundled FirstOrder.Language.Structure Finite CategoryTheory.Bundled.α	—	FirstOrder.Language.IsFraisseLimit.isFraisse FirstOrder.Language.Countable.countable_functions Encodable.countable instCountableULift instCountableNat isFraisseLimit_of_countable_infinite instInfiniteULift instInfiniteNat

---

← Back to Index