injective — Mathlib

English

If iSupIndep t holds and t i ≠ ⊥ for all i, then t is injective.

Русский

Если iSupIndep t выполняется и для всех i t i ≠ ⊥, тогда t инъективна.

LaTeX

$$$iSupIndep(t) \\\\land (\\\\forall i, t(i) \\neq ⊥) \\\\Rightarrow Injective(t)$$$

Lean4

theorem injective (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Injective t :=
  by
  suffices univ = {i | t i ≠ ⊥} by rw [injective_iff_injOn_univ, this]; exact ht.injOn
  simp_all

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