preimage_subset_image_of_inverse — Mathlib

English

Under a LeftInverse relation, the preimage of a set s is contained in the image under the inverse: f^{-1}' s ⊆ g '' s.

Русский

При ленивом обратном отношении предобраз множества s содержится в образе через обратную функцию: f^{-1}' s ⊆ g '' s.

LaTeX

$$$ f^{-1}' s \\subseteq g '' s. $$$

Lean4

theorem preimage_subset_image_of_inverse {f : α → β} {g : β → α} (I : LeftInverse g f) (s : Set β) : f ⁻¹' s ⊆ g '' s :=
  fun b h => ⟨f b, h, I b⟩

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