English
iSupIndep (i → t i ≠ ⊥) is equivalent to iSupIndep t.
Русский
Эквивалентны iSupIndep на подмножестве индексов, где элементы не равны ⊥, и iSupIndep t.
LaTeX
$$$iSupIndep\\left(\\\\lambda i:{i \\to α}.$$$$
Lean4
@[simp]
theorem iSupIndep_ne_bot : iSupIndep (fun i : { i // t i ≠ ⊥ } ↦ t i) ↔ iSupIndep t :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩
simp only [iSupIndep_def] at h ⊢
intro i
cases eq_or_ne (t i) ⊥ with
| inl hi => simp [hi]
| inr hi => ?_
convert h ⟨i, hi⟩
have : ∀ j, ⨆ (_ : t j = ⊥), t j = ⊥ := fun j ↦ by simp only [iSup_eq_bot, imp_self]
rw [iSup_split _ (fun j ↦ t j = ⊥), iSup_subtype]
simp only [iSup_comm (ι' := _ ≠ i), this, ne_eq, sup_of_le_right, Subtype.mk.injEq, iSup_bot, bot_le]
