preimage_subset_preimage_iff — Mathlib

English

If s ⊆ range f, then f^{-1}(s) ⊆ f^{-1}(t) ↔ s ⊆ t.

Русский

Если s ⊆ range(f), то f^{-1}(s) ⊆ f^{-1}(t) эквивалентно s ⊆ t.

LaTeX

$$$ s \\subseteq \\mathrm{range}(f) \\Rightarrow (f^{-1}(s) \\subseteq f^{-1}(t) \\iff s \\subseteq t). $$$

Lean4

@[simp]
theorem preimage_subset_preimage_iff {s t : Set α} {f : β → α} (hs : s ⊆ range f) : f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t :=
  by
  constructor
  · intro h x hx
    rcases hs hx with ⟨y, rfl⟩
    exact h hx
  intro h x; apply h

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