inv — Mathlib

English

If f is a map between sets and β has an involutive inverse, then mapping by f⁻¹ sends A to B⁻¹ whenever f sends A to B.

Русский

Если f — отображение между множествами и β имеет инволютивно-обратимый элемент, тогда отображение через f⁻¹ отправляет A в B⁻¹, если f отправляет A в B.

LaTeX

$$MapsTo f A B → MapsTo f^{-1} A B^{-1}$$

Lean4

@[to_additive]
theorem inv [InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) : MapsTo (f⁻¹) A (B⁻¹) :=
  fun _ ha => inv_mem_inv.2 (h ha)

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