image_inter' — Mathlib

English

If hf is a LeftInvOn, then f''(s₁ ∩ s) equals f'⁻¹(s₁ ∩ s) ∩ f''s.

Русский

Если hf — левый обратный, то образ пересечения равен пересечению предобраза и образа.

LaTeX

$$$$ f''(s_1 \\cap s) = f'^{-1}(s_1 \\cap s) \\cap f''s. $$$$

Lean4

theorem image_inter' (hf : LeftInvOn f' f s) : f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s :=
  by
  apply Subset.antisymm
  · rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩
    exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩
  · rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩
    exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩

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