preimage_image_inter — Mathlib

English

For InjOn f on u, f⁻¹'(f'' s1) ∩ s = s1 whenever s1 ⊆ s ⊆ u.

Русский

Для InjOn f на u выполняется f⁻¹'(f'' s1) ∩ s = s1, когда s1 ⊆ s ⊆ u.

LaTeX

$$$ \\forall s, s_1, s_2, (hf : \\operatorname{InjOn} f u) (hs : s_1 \\subseteq u) (ht : s_2 \\subseteq u) : f^{-1}'(f'' s_1) \\cap s_2 = s_1$$$

Lean4

theorem preimage_image_inter (hf : InjOn f s) (hs : s₁ ⊆ s) : f ⁻¹' (f '' s₁) ∩ s = s₁ :=
  ext fun _ => ⟨fun ⟨h₁, h₂⟩ => hf.mem_of_mem_image hs h₂ h₁, fun h => ⟨mem_image_of_mem _ h, hs h⟩⟩

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