subset_right — Mathlib

English

If f is bijective on s to t and r ⊆ t, then f maps s ∩ f⁻¹(r) bijectively onto r.

Русский

Если f биективна на s→t и r ⊆ t, тогда f отображает s ∩ f⁻¹(r) биективно на r.

LaTeX

$$$\\text{BijOn}(f,s,t) \\land r\\subseteq t \\Rightarrow \\text{BijOn}(f\\cap s, r)$$$

Lean4

theorem subset_right {r : Set β} (hf : BijOn f s t) (hrt : r ⊆ t) : BijOn f (s ∩ f ⁻¹' r) r :=
  by
  refine ⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩
  obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)
  exact ⟨y, ⟨hy, hx⟩, rfl⟩

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