Commit 2023-03-24 13:23 0e24dac4

View on Github →

feat: port LinearAlgebra.AffineSpace.AffineSubspace (#2923)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

added theorem AffineEquiv.span_eq_top_iff

added theorem AffineMap.lineMap_mem

added theorem AffineMap.lineMap_mem_affineSpan_pair

added theorem AffineMap.lineMap_rev_mem_affineSpan_pair

added theorem AffineMap.map_top_of_surjective

added theorem AffineMap.span_eq_top_of_surjective

added theorem AffineMap.vectorSpan_image_eq_submodule_map

added theorem AffineSubspace.Parallel.direction_eq

added theorem AffineSubspace.Parallel.refl

added theorem AffineSubspace.Parallel.symm

added theorem AffineSubspace.Parallel.trans

added theorem AffineSubspace.Parallel.vectorSpan_eq

added def AffineSubspace.Parallel

added theorem AffineSubspace.affineSpan_coe

added theorem AffineSubspace.affineSpan_eq_infₛ

added theorem AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty

added theorem AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial

added theorem AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq

added theorem AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty

added theorem AffineSubspace.bot_coe

added theorem AffineSubspace.bot_ne_top

added theorem AffineSubspace.bot_parallel_iff_eq_bot

added theorem AffineSubspace.card_pos_of_affineSpan_eq_top

added theorem AffineSubspace.coeSubtype

added theorem AffineSubspace.coe_affineSpan_singleton

added theorem AffineSubspace.coe_comap

added theorem AffineSubspace.coe_direction_eq_vsub_set

added theorem AffineSubspace.coe_direction_eq_vsub_set_left

added theorem AffineSubspace.coe_direction_eq_vsub_set_right

added theorem AffineSubspace.coe_eq_bot_iff

added theorem AffineSubspace.coe_eq_univ_iff

added theorem AffineSubspace.coe_injective

added theorem AffineSubspace.coe_map

added theorem AffineSubspace.coe_vadd

added theorem AffineSubspace.coe_vsub

added def AffineSubspace.comap

added theorem AffineSubspace.comap_comap

added theorem AffineSubspace.comap_id

added theorem AffineSubspace.comap_inf

added theorem AffineSubspace.comap_mono

added theorem AffineSubspace.comap_span

added theorem AffineSubspace.comap_supr

added theorem AffineSubspace.comap_symm

added theorem AffineSubspace.comap_top

added def AffineSubspace.direction

added def AffineSubspace.directionOfNonempty

added theorem AffineSubspace.directionOfNonempty_eq_direction

added theorem AffineSubspace.direction_affineSpan_insert

added theorem AffineSubspace.direction_bot

added theorem AffineSubspace.direction_eq_top_iff_of_nonempty

added theorem AffineSubspace.direction_eq_vectorSpan

added theorem AffineSubspace.direction_inf

added theorem AffineSubspace.direction_inf_of_mem

added theorem AffineSubspace.direction_inf_of_mem_inf

added theorem AffineSubspace.direction_le

added theorem AffineSubspace.direction_lt_of_nonempty

added theorem AffineSubspace.direction_mk'

added theorem AffineSubspace.direction_sup

added theorem AffineSubspace.direction_top

added theorem AffineSubspace.eq_bot_or_nonempty

added theorem AffineSubspace.eq_iff_direction_eq_of_mem

added theorem AffineSubspace.eq_of_direction_eq_of_nonempty_of_le

added theorem AffineSubspace.eq_univ_of_subsingleton_span_eq_top

added theorem AffineSubspace.exists_of_lt

added theorem AffineSubspace.ext

added theorem AffineSubspace.ext_iff

added theorem AffineSubspace.ext_of_direction_eq

added theorem AffineSubspace.gc_map_comap

added theorem AffineSubspace.inf_coe

added theorem AffineSubspace.injective_subtype

added theorem AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl

added theorem AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top

added theorem AffineSubspace.le_comap_map

added theorem AffineSubspace.le_def'

added theorem AffineSubspace.le_def

added theorem AffineSubspace.lt_def

added theorem AffineSubspace.lt_iff_le_and_exists

added def AffineSubspace.map

added theorem AffineSubspace.map_bot

added theorem AffineSubspace.map_comap_le

added theorem AffineSubspace.map_direction

added theorem AffineSubspace.map_eq_bot_iff

added theorem AffineSubspace.map_id

added theorem AffineSubspace.map_le_iff_le_comap

added theorem AffineSubspace.map_map

added theorem AffineSubspace.map_span

added theorem AffineSubspace.map_sup

added theorem AffineSubspace.map_supᵢ

added theorem AffineSubspace.map_symm

added theorem AffineSubspace.mem_affineSpan_insert_iff

added theorem AffineSubspace.mem_affineSpan_singleton

added theorem AffineSubspace.mem_coe

added theorem AffineSubspace.mem_comap

added theorem AffineSubspace.mem_direction_iff_eq_vsub

added theorem AffineSubspace.mem_direction_iff_eq_vsub_left

added theorem AffineSubspace.mem_direction_iff_eq_vsub_right

added theorem AffineSubspace.mem_inf_iff

added theorem AffineSubspace.mem_map

added theorem AffineSubspace.mem_map_iff_mem_of_injective

added theorem AffineSubspace.mem_map_of_mem

added theorem AffineSubspace.mem_mk'_iff_vsub_mem

added theorem AffineSubspace.mem_top

added def AffineSubspace.mk'

added theorem AffineSubspace.mk'_eq

added theorem AffineSubspace.mk'_nonempty

added theorem AffineSubspace.nonempty_iff_ne_bot

added theorem AffineSubspace.nonempty_of_affineSpan_eq_top

added theorem AffineSubspace.not_le_iff_exists

added theorem AffineSubspace.not_mem_bot

added theorem AffineSubspace.parallel_bot_iff_eq_bot

added theorem AffineSubspace.parallel_comm

added theorem AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

added theorem AffineSubspace.preimage_coe_affineSpan_singleton

added theorem AffineSubspace.self_mem_mk'

added theorem AffineSubspace.spanPoints_subset_coe_of_subset_coe

added theorem AffineSubspace.span_empty

added theorem AffineSubspace.span_union

added theorem AffineSubspace.span_unionᵢ

added theorem AffineSubspace.span_univ

added theorem AffineSubspace.subsingleton_of_subsingleton_span_eq_top

added theorem AffineSubspace.subtype_apply

added theorem AffineSubspace.subtype_linear

added theorem AffineSubspace.sup_direction_le

added theorem AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty

added def AffineSubspace.toAddTorsor

added theorem AffineSubspace.top_coe

added theorem AffineSubspace.vadd_mem_iff_mem_direction

added theorem AffineSubspace.vadd_mem_iff_mem_of_mem_direction

added theorem AffineSubspace.vadd_mem_mk'

added theorem AffineSubspace.vadd_mem_of_mem_direction

added theorem AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top

added theorem AffineSubspace.vsub_left_mem_direction_iff_mem

added theorem AffineSubspace.vsub_mem_direction

added theorem AffineSubspace.vsub_right_mem_direction_iff_mem

added structure AffineSubspace

added def Submodule.toAffineSubspace

added def affineSpan

added theorem affineSpan_coe_preimage_eq_top

added theorem affineSpan_eq_bot

added theorem affineSpan_induction'

added theorem affineSpan_induction

added theorem affineSpan_insert_affineSpan

added theorem affineSpan_insert_eq_affineSpan

added theorem affineSpan_le

added theorem affineSpan_mono

added theorem affineSpan_nonempty

added theorem affineSpan_pair_le_of_left_mem

added theorem affineSpan_pair_le_of_mem_of_mem

added theorem affineSpan_pair_le_of_right_mem

added theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top

added theorem bot_lt_affineSpan

added theorem coe_affineSpan

added theorem direction_affineSpan

added theorem left_mem_affineSpan_pair

added theorem mem_affineSpan

added theorem mem_spanPoints

added theorem mem_vectorSpan_pair

added theorem mem_vectorSpan_pair_rev

added theorem right_mem_affineSpan_pair

added theorem smul_vsub_mem_vectorSpan_pair

added theorem smul_vsub_rev_mem_vectorSpan_pair

added theorem smul_vsub_rev_vadd_mem_affineSpan_pair

added theorem smul_vsub_vadd_mem_affineSpan_pair

added def spanPoints

added theorem spanPoints_nonempty

added theorem subset_affineSpan

added theorem subset_spanPoints

added theorem vadd_left_mem_affineSpan_pair

added theorem vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan

added theorem vadd_right_mem_affineSpan_pair

added def vectorSpan

added theorem vectorSpan_def

added theorem vectorSpan_empty

added theorem vectorSpan_eq_span_vsub_finset_right_ne

added theorem vectorSpan_eq_span_vsub_set_left

added theorem vectorSpan_eq_span_vsub_set_left_ne

added theorem vectorSpan_eq_span_vsub_set_right

added theorem vectorSpan_eq_span_vsub_set_right_ne

added theorem vectorSpan_image_eq_span_vsub_set_left_ne

added theorem vectorSpan_image_eq_span_vsub_set_right_ne

added theorem vectorSpan_insert_eq_vectorSpan

added theorem vectorSpan_mono

added theorem vectorSpan_pair

added theorem vectorSpan_pair_rev

added theorem vectorSpan_range_eq_span_range_vsub_left

added theorem vectorSpan_range_eq_span_range_vsub_left_ne

added theorem vectorSpan_range_eq_span_range_vsub_right

added theorem vectorSpan_range_eq_span_range_vsub_right_ne

added theorem vectorSpan_singleton

added theorem vsub_mem_vectorSpan

added theorem vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints

added theorem vsub_mem_vectorSpan_pair

added theorem vsub_rev_mem_vectorSpan_pair

added theorem vsub_set_subset_vectorSpan