notMem_range_coe_iff — Mathlib

English

An element x ∈ OnePoint X lies outside the image of X under the canonical embedding if and only if x = ∞.

Русский

Элемент x ∈ OnePoint X лежит вне образа X под каноническим вложением тогда и только тогда, когда x = ∞.

LaTeX

$$$x \\notin \\iota''X \\iff x = \\infty.$$$

Lean4

theorem notMem_range_coe_iff {x : OnePoint X} : x ∉ range some ↔ x = ∞ := by
  rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]

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