isDecompOn — Mathlib

English

The theorem states that for any f: Equidecomp X G, f is an IsDecompOn on f.toFun restricted to f.source with f.witness as the witnessing set.

Русский

Теорема утверждает, что для любого f: Equidecomp X G, f является IsDecompOn на f.toFun, ограниченном по f.source, при помощи f.witness как свидетеля.

LaTeX

$$$\text{Equidecomp.isDecompOn}(f) : \mathrm{IsDecompOn}\; f.toFun\; f.source\; f.witness.$$$

Lean4

theorem isDecompOn (f : Equidecomp X G) : IsDecompOn f f.source f.witness :=
  f.isDecompOn'.choose_spec

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