prop_of_isGood_of_contained — Mathlib

English

The projection π C (ord I · < o) is a closed map when C is closed.

Русский

Проекция π C (ord I · < o) является замкнутым отображением, если C замкнуто.

LaTeX

$$$\\text{IsClosed}(C) \\Rightarrow \\text{IsClosed}(\\pi C (\\mathrm{ord}\\,I\\cdot < o)).$$$

Lean4

theorem prop_of_isGood_of_contained {l : Products I} (o : Ordinal) (h : l.isGood C) (hsC : contained C o) (i : I)
    (hi : i ∈ l.val) : ord I i < o := by
  by_contra h'
  apply h
  suffices eval C l = 0 by simp [this]
  ext x
  simp only [eval_eq, LocallyConstant.coe_zero, Pi.zero_apply, ite_eq_right_iff, one_ne_zero]
  contrapose! h'
  exact hsC x.val x.prop i (h'.1 i hi)

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