Theorems · Definition · geometry

Projectivization.Subspace.mk.noConfusion

{K : Type u_1} →
  {V : Type u_2} →
    {inst : DivisionRing K} →
      {inst_1 : AddCommGroup V} →
        {inst_2 : Module K V} →
          {P : Sort u} →
            {carrier : Set (Projectivization K V)} →
              {mem_add' :
                  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
                    Projectivization.mk K v hv ∈ carrier →
                      Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier} →
                {carrier' : Set (Projectivization K V)} →
                  {mem_add'' :
                      ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
                        Projectivization.mk K v hv ∈ carrier' →
                          Projectivization.mk K w hw ∈ carrier' → Projectivization.mk K (v + w) hvw ∈ carrier'} →
                    { carrier := carrier, mem_add' := mem_add' } = { carrier := carrier', mem_add' := mem_add'' } →
                      (carrier ≍ carrier' → P) → P

Defined in

Mathlib.LinearAlgebra.Projectivization.Subspace

Cited by

1 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound