proj_fiber — Mathlib

English

For x : hs.Quotient, the fiber of hs.proj over {x} equals s(hs.equivQuotient.symm x); i.e., hs.proj^{-1}({x}) = s (hs.equivQuotient.symm x).

Русский

Для x ∈ hs.Quotient множество проекции над единичным классом равно s(hs.equivQuotient.symm x).

LaTeX

$$$ hs.proj^{-1}'(\{x\}) = s (hs.equivQuotient.symm x) $$$

Lean4

theorem proj_fiber (x : hs.Quotient) : hs.proj ⁻¹' { x } = s (hs.equivQuotient.symm x) :=
  Quotient.inductionOn' x fun x => by
    ext y
    simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]
    exact Quotient.eq''

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