mem_cutMap_iff — Mathlib

English

Membership in cutMap can be characterized by rationals: b ∈ cutMap β a iff ∃ q ∈ ℚ with (q : α) < a and (q : β) = b.

Русский

Членство в cutMap β a эквивалентно существованию рационала q: (q : α) < a и (q : β) = b.

LaTeX

$$$b \in \operatorname{cutMap}_{β} a \iff \exists q \in \mathbb{Q}, (q : α) < a \land (q : β) = b$$$

Lean4

@[simp]
theorem mem_cutMap_iff : b ∈ cutMap β a ↔ ∃ q : ℚ, (q : α) < a ∧ (q : β) = b :=
  Iff.rfl

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