exists_conts_b_of_den — Mathlib

English

If g.dens n = B for some B ∈ K, then there exists conts with conts.n = conts and conts.b = B.

Русский

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

LaTeX

$$$g.dens n = B \\Rightarrow \\exists conts, \\ g.conts n = conts \\land conts.b = B$$$

Lean4

theorem exists_conts_b_of_den {B : K} (nth_denom_eq : g.dens n = B) : ∃ conts, g.conts n = conts ∧ conts.b = B := by
  simpa

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