preimage_subset_preimage — Mathlib

English

The preimage under the inverse relation equals the image under the forward relation: R.inv.preimage s = image R s.

Русский

Предобразование по обратному отношению равно образу по прямому отношению: R.inv.preimage s = image R s.

LaTeX

$$R.inv.preimage\,s = image\,R\,s$$

Lean4

@[gcongr]
theorem preimage_subset_preimage (ht : t₁ ⊆ t₂) : preimage R t₁ ⊆ preimage R t₂ := fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ht ha, hab⟩

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