exists_s_a_of_partNum — Mathlib

English

If g.partNums.get? n = some a, then there exists gp with g.s.get? n = some gp and gp.a = a.

Русский

Если g.partNums.get? n = some a, то существует gp такое, что g.s.get? n = some gp и gp.a = a.

LaTeX

$$$$ \forall {a : K}, \ g.partNums.get? n = \text{some } a \Rightarrow \exists gp, g.s.get? n = \text{some } gp \land gp.a = a. $$$$

Lean4

theorem exists_s_a_of_partNum {a : α} (nth_partNum_eq : g.partNums.get? n = some a) :
    ∃ gp, g.s.get? n = some gp ∧ gp.a = a := by simpa [partNums, Stream'.Seq.map_get?] using nth_partNum_eq

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