exists_s_b_of_partDen — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_s_b_of_partDen {b : α} (nth_partDen_eq : g.partDens.get? n = some b) :
    ∃ gp, g.s.get? n = some gp ∧ gp.b = b := by simpa [partDens, Stream'.Seq.map_get?] using nth_partDen_eq

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