mem_coe — Mathlib

English

A point belongs to an affine subspace as a set if and only if it belongs to the subspace itself.

Русский

Точка принадлежит аффинному подпространству как множеству тогда и только тогда, когда она принадлежит самому подпространству.

LaTeX

$$$p \\in (s : Set\\ P) \\iff p \\in s$$$

Lean4

/-- A point is in an affine subspace coerced to a set if and only if it is in that affine
subspace. -/
theorem mem_coe (p : P) (s : AffineSubspace k P) : p ∈ (s : Set P) ↔ p ∈ s := by simp

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