isSeparableContraction — Mathlib

English

The chosen contraction hf.contraction is indeed a separable contraction of f.

Русский

Выбранная конракция hf.contraction действительно является разделимой конракцией f.

LaTeX

$$$\\text{IsSeparableContraction}_q(f, hf.contraction)$$$

Lean4

/-- The `HasSeparableContraction.contraction` is indeed a separable contraction. -/
theorem isSeparableContraction : IsSeparableContraction q f hf.contraction :=
  Classical.choose_spec hf

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