contained_eq_proj — Mathlib

English

If C is contained in o, then C equals the projection π C on ord I · < o.

Русский

Если C содержится в o, тогда C равно проекции π C на ord I · < o.

LaTeX

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

Lean4

theorem contained_eq_proj (o : Ordinal) (h : contained C o) : C = π C (ord I · < o) :=
  by
  have := proj_prop_eq_self C (ord I · < o)
  simp only [ne_eq, Bool.not_eq_false, π] at this
  exact (this (fun i x hx ↦ h x hx i)).symm

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