sigma_map_iff — Mathlib

English

Let f1: α1 → α2 be injective. Then Sigma.map f1 f2 is injective iff for every a: α1, f2 a is injective.

Русский

Пусть f1: α1 → α2 инъективен. Тогда Sigma.map f1 f2 инъективно тогда и только тогда, когда для каждого a: α1 отображение f2 a инъективно.

LaTeX

$$$\\operatorname{Injective} f_1 \\rightarrow \\left( \\operatorname{Injective}(\\Sigma\\text{map } f_1 f_2) \\iff \\forall a, \\operatorname{Injective}(f_2 a) \\right).$$$

Lean4

theorem sigma_map_iff {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h₁ : Injective f₁) :
    Injective (Sigma.map f₁ f₂) ↔ ∀ a, Injective (f₂ a) :=
  ⟨fun h ↦ h.of_sigma_map, h₁.sigma_map⟩

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