comp' — Mathlib

English

If iSupIndep of t ∘ f holds and f is surjective, then iSupIndep t holds.

Русский

Если iSupIndep от t ∘ f верно и f сюръективна, тогда iSupIndep t верно.

LaTeX

$$$\\\\forall ι ι',\\\\ {t: ι \\to α}\\\\ {f: ι' \\to ι},\\\\ iSupIndep(t \\circ f) \\\\land Surjective(f) \\\\Rightarrow iSupIndep(t)$$$

Lean4

theorem comp' {ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep <| t ∘ f) (hf : Surjective f) : iSupIndep t :=
  by
  intro i
  obtain ⟨i', rfl⟩ := hf i
  rw [← hf.iSup_comp]
  exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

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