image_subset_preimage_of_inverse — Mathlib

English

If I is a LeftInverse of g with f, then f'' s ⊆ g '' s for any s ⊆ α.

Русский

Если I является левым обратным для g относительно f, тогда f'' s ⊆ g '' s для любого s ⊆ α.

LaTeX

$$$ f'' s \\subseteq g '' s \\quad \\text{for } s \\subseteq α, \\text{ given } I: \\text{LeftInverse } g f. $$$

Lean4

theorem image_subset_preimage_of_inverse {f : α → β} {g : β → α} (I : LeftInverse g f) (s : Set α) : f '' s ⊆ g ⁻¹' s :=
  fun _ ⟨a, h, e⟩ => e ▸ ((I a).symm ▸ h : g (f a) ∈ s)

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