fg_substructure — Mathlib

English

If S is a finitely generated L-substructure of M, then the corresponding bundled substructure lies in the age of M.

Русский

Если S является FG-подструктурой M, то соответствующая зафиксированная подструктура принадлежит возрасту M.

LaTeX

$$$S\ FG \rightarrow Bundled.mk S \in L.age M$$$

Lean4

theorem fg_substructure {S : L.Substructure M} (fg : S.FG) : Bundled.mk S ∈ L.age M := by
  exact ⟨(Substructure.fg_iff_structure_fg _).1 fg, ⟨subtype _⟩⟩

Похожие утверждения