Partial — Mathlib

English

The type HahnEmbedding.Partial encodes all partial Hahn embeddings with coefficients in Lex HahnSeries.

Русский

Тип HahnEmbedding.Partial кодирует все частичные вложения Хаана с коэффициентами в Лекс-ряд Хаана.

LaTeX

$$$\text{HahnEmbedding.Partial} := \{ f : M \to\!.[K]\ Lex (HahnSeries(\text{FiniteArchimedeanClass } M) R) // IsPartial seed f\}$$$

Lean4

/-- The type of all partial Hahn embeddings. -/
abbrev Partial :=
  { f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R) // IsPartial seed f }

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