mem_image_iff_of_inverse — Mathlib

English

Let f: α → β and g: β → α with g f = id_A and f g = id_B. Then for any subset S ⊆ α and any b ∈ β, b ∈ f[S] if and only if g(b) ∈ S.

Русский

Пусть f: A → B и g: B → A удовлетворяют g ∘ f = id_A и f ∘ g = id_B. Тогда для любого подмножества S ⊆ A и любого b ∈ B выполняется b ∈ f[S] ⇔ g(b) ∈ S.

LaTeX

$$$$ \forall S \subseteq A,\ \forall b \in B:\, b \in f[S] \iff g(b) \in S. $$$$

Lean4

theorem mem_image_iff_of_inverse {f : α → β} {g : β → α} {b : β} {s : Set α} (h₁ : LeftInverse g f)
    (h₂ : RightInverse g f) : b ∈ f '' s ↔ g b ∈ s := by rw [image_eq_preimage_of_inverse h₁ h₂]; rfl

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