prop_of_isGood — Mathlib

English

If l is Good with respect to π C J, then J holds on every i in l.val.

Русский

Если l хорошо с отношением к π C J, то J верно на каждом индексе i из l.val.

LaTeX

$$$l.\\mathrm{isGood}(\\pi C J) \\implies ∀ i,\\; i ∈ l.val → J i.$$$

Lean4

theorem prop_of_isGood {l : Products I} (J : I → Prop) [∀ j, Decidable (J j)] (h : l.isGood (π C J)) :
    ∀ a, a ∈ l.val → J a := by
  intro i hi
  by_contra h'
  apply h
  suffices eval (π C J) l = 0 by
    rw [this]
    exact Submodule.zero_mem _
  ext ⟨_, _, _, rfl⟩
  rw [eval_eq, if_neg fun h ↦ ?_, LocallyConstant.zero_apply]
  simpa [Proj, h'] using h i hi

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