apply_mem — Mathlib

English

If h is QuasispectrumRestricts a f, then for any s ∈ quasispectrum S a, f(s) ∈ quasispectrum R a.

Русский

Если h — ограничение квазиспеktrа a через f, тогда для любого s ∈ quasispectrum S a, f(s) ∈ quasispectrum R a.

LaTeX

$$$\\text{If } h:\\mathrm{QuasispectrumRestricts}(a,f), \\text{ then } \\forall s \\in \\mathrm{quasispectrum}(S,a),\\; f(s) \\in \\mathrm{quasispectrum}(R,a)$$$

Lean4

theorem apply_mem (h : QuasispectrumRestricts a f) {s : S} (hs : s ∈ quasispectrum S a) : f s ∈ quasispectrum R a :=
  h.image ▸ ⟨s, hs, rfl⟩

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