pi_inj — Mathlib

English

If π f1 = π f2 then f1 = f2, provided all f1 i are non-bottom.

Русский

Если π f1 = π f2, то f1 = f2, при условии, что все f1 i непротиворечивы.

LaTeX

$$$(∀ i, (f_1 i).NeBot) \\Rightarrow (\\pi f_1 = \\pi f_2) \\Rightarrow (f_1 = f_2)$$$

Lean4

@[simp]
theorem pi_inj [∀ i, NeBot (f₁ i)] : pi f₁ = pi f₂ ↔ f₁ = f₂ :=
  by
  refine ⟨fun h => ?_, congr_arg pi⟩
  have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
  haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
  exact hle.antisymm (pi_le_pi.1 h.ge)

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