instSetLike — Mathlib

English

If two subspaces A and B have the same underlying set of projective points, then A = B.

Русский

Если два подпространства A и B имеют одинаковое множество точек в проективном пространстве, то A = B.

LaTeX

$$$A=B \iff A.\mathrm{carrier}=B.\mathrm{carrier}$$$

Lean4

instance : SetLike (Subspace K V) (ℙ K V) where
  coe := carrier
  coe_injective' A
    B := by
    cases A
    cases B
    simp

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