preimage' — Mathlib

English

If s is nonempty and s ⊆ range f, then f^{-1}(s) is nonempty.

Русский

Если s ненулево непусто и s ⊆ range f, то f^{-1}(s) ненулево непусто.

LaTeX

$$$ s.\\operatorname{Nonempty} \\land s \\subseteq \\operatorname{range} f \\Rightarrow (f^{-1}' s).\\operatorname{Nonempty}$$$

Lean4

theorem preimage' {s : Set β} (hs : s.Nonempty) {f : α → β} (hf : s ⊆ range f) : (f ⁻¹' s).Nonempty :=
  let ⟨_, hy⟩ := hs
  let ⟨x, hx⟩ := hf hy
  ⟨x, by grind⟩

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