injOn — Mathlib

English

iSupIndep t implies t is injective on the non-bottom indices.

Русский

iSupIndep t подразумевает, что t инъективна на множестве индексов, где t i ≠ ⊥.

LaTeX

$$$iSupIndep(t) \\\\Rightarrow InjOn(t, {i \\mid t(i) \\neq ⊥})$$$

Lean4

theorem injOn (ht : iSupIndep t) : InjOn t {i | t i ≠ ⊥} :=
  by
  rintro i _ j (hj : t j ≠ ⊥) h
  by_contra! contra
  apply hj
  suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
    replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht
  replace contra : j ≠ i := Ne.symm contra
  exact le_iSup₂ (f := fun x _ ↦ t x) j contra

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