mem_of_mem_image — Mathlib

English

If f is injOn on s and s1 ⊆ s and x ∈ s and f x ∈ f '' s1, then x ∈ s1.

Русский

Если f инъективна на s, и s1 ⊆ s, и x ∈ s, и f x ∈ f '' s1, то x ∈ s1.

LaTeX

$$$ \\forall x, (\\operatorname{InjOn} f s) \\land (s_1 \\subseteq s) \\land (x \\in s) \\land (f x \\in f '' s_1) \\Rightarrow x \\in s_1$$$

Lean4

theorem mem_of_mem_image {x} (hf : InjOn f s) (hs : s₁ ⊆ s) (h : x ∈ s) (h₁ : f x ∈ f '' s₁) : x ∈ s₁ :=
  let ⟨_, h', Eq⟩ := h₁
  hf (hs h') h Eq ▸ h'

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