div — Mathlib

English

If f1 maps A to B1 and f2 maps A to B2, then the quotient map f1 / f2 maps A to B1 / B2.

Русский

Если f1 отображает A в B1 и f2 отображает A в B2, то отображение деления f1 / f2 отправляет A в B1 / B2.

LaTeX

$$MapsTo f1 A B1 → MapsTo f2 A B2 → MapsTo (f1 / f2) A (B1 / B2)$$

Lean4

@[to_additive]
theorem div [Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
    MapsTo (f₁ / f₂) A (B₁ / B₂) := fun _ ha => div_mem_div (h₁ ha) (h₂ ha)

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