image_inter — Mathlib

English

If hf is a LeftInvOn f' f s, then f''(s₁ ∩ s) = 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₁ ∩ s) ∩ f '' s :=
  by
  rw [hf.image_inter']
  refine Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))
  rintro _ ⟨h₁, x, hx, rfl⟩; exact ⟨⟨h₁, by rwa [hf hx]⟩, mem_image_of_mem _ hx⟩

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