exists_conts_a_of_num — Mathlib

English

If g.nums n = A for some A ∈ K, then there exists conts such that g.conts n = conts and conts.a = A.

Русский

Если g.nums n = A для некоторого A ∈ K, существует conts, такой что g.conts n = conts и conts.a = A.

LaTeX

$$$g.nums n = A \\Rightarrow \\exists conts, \\ g.conts n = conts \\land conts.a = A$$$

Lean4

theorem exists_conts_a_of_num {A : K} (nth_num_eq : g.nums n = A) : ∃ conts, g.conts n = conts ∧ conts.a = A := by simpa

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