sampleableExt — Mathlib

English

The set of injective functions from integers to integers admits a sampleable extension, i.e., there is a structure that allows random sampling from injective maps ℤ → ℤ.

Русский

Множество инъективных отображений ℤ → ℤ допускает образование структуры, позволяющей случайную выборку таких отображений.

LaTeX

$$$\text{SampleableExt}(\{ f:\mathbb{Z}\to\mathbb{Z}\mid \text{Injective}(f)\})$$$

Lean4

instance sampleableExt : SampleableExt { f : ℤ → ℤ // Function.Injective f }
    where
  proxy := InjectiveFunction ℤ
  interp f := ⟨apply f, f.injective⟩
  shrink := { shrink := @InjectiveFunction.shrink ℤ _ }

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