fst — Mathlib

English

If x lies in M ⊔ ⟨y⟩, then x decomposes as x = m + r y for some m ∈ domain and r ∈ R; fst selects such an m.

Русский

Если x ∈ M ⊔ ⟨y⟩, то x = m + r y для некоторого m в домене и r ∈ R; fst выбирает такое m.

LaTeX

$$$ \forall x\in M \oplus \langle y\rangle: \exists m\in \mathrm{domain}, \exists r\in R: x = m + r y$; fst(x) = m$$

Lean4

/-- If `x ∈ M ⊔ ⟨y⟩`, then `x = m + r • y`, `fst` pick an arbitrary such `m`. -/
def fst {y : N} (x : supExtensionOfMaxSingleton i f y) : (extensionOfMax i f).domain :=
  (extensionOfMax_adjoin.aux1 i x).choose

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