English
An induction principle for Projectivization: to prove a property P for every p ∈ ℙ_K(V), it suffices to show P(mk K v hv) for every v ≠ 0.
Русский
Принцип индукции по проективному пространству: чтобы доказать свойство P для каждого p ∈ ℙ_K(V), достаточно показать P( mk K v hv ) для каждого ненулевого вектора v.
LaTeX
$$$ \forall P : \mathbb{P}_K(V) \to \mathrm{Prop},\ (\forall v \neq 0, P(\mathrm mk\ K\ v\ hv)) \Rightarrow \forall p, P(p) $$$
Lean4
/-- An induction principle for `Projectivization`. Use as `induction v`. -/
@[elab_as_elim, cases_eliminator, induction_eliminator]
theorem ind {P : ℙ K V → Prop} (h : ∀ (v : V) (h : v ≠ 0), P (mk K v h)) : ∀ p, P p :=
Quotient.ind' <| Subtype.rec <| h
