English
The ≤ order on subspaces coincides with the subset relation.
Русский
Порядок ≤ на подпространствах совпадает с отношением подмножества.
LaTeX
$$$s_1 \\le s_2 \\iff (s_1 : Set P) \\subseteq s_2$$$
Lean4
instance : CompleteLattice (AffineSubspace k P) :=
{
PartialOrder.lift ((↑) : AffineSubspace k P → Set P)
coe_injective with
sup := fun s₁ s₂ => affineSpan k (s₁ ∪ s₂)
le_sup_left := fun _ _ => Set.Subset.trans Set.subset_union_left (subset_spanPoints k _)
le_sup_right := fun _ _ => Set.Subset.trans Set.subset_union_right (subset_spanPoints k _)
sup_le := fun _ _ _ hs₁ hs₂ => spanPoints_subset_coe_of_subset_coe (Set.union_subset hs₁ hs₂)
inf := fun s₁ s₂ =>
mk (s₁ ∩ s₂) fun c _ _ _ hp₁ hp₂ hp₃ =>
⟨s₁.smul_vsub_vadd_mem c hp₁.1 hp₂.1 hp₃.1, s₂.smul_vsub_vadd_mem c hp₁.2 hp₂.2 hp₃.2⟩
inf_le_left := fun _ _ => Set.inter_subset_left
inf_le_right := fun _ _ => Set.inter_subset_right
le_sInf := fun S s₁ hs₁ => by
apply Set.subset_sInter
rintro t ⟨s, _hs, rfl⟩
exact Set.subset_iInter (hs₁ s)
top :=
{ carrier := Set.univ
smul_vsub_vadd_mem := fun _ _ _ _ _ _ _ => Set.mem_univ _ }
le_top := fun _ _ _ => Set.mem_univ _
bot :=
{ carrier := ∅
smul_vsub_vadd_mem := fun _ _ _ _ => False.elim }
bot_le := fun _ _ => False.elim
sSup := fun s => affineSpan k (⋃ s' ∈ s, (s' : Set P))
sInf := fun s =>
mk (⋂ s' ∈ s, (s' : Set P)) fun c p₁ p₂ p₃ hp₁ hp₂ hp₃ =>
Set.mem_iInter₂.2 fun s₂ hs₂ => by
rw [Set.mem_iInter₂] at *
exact s₂.smul_vsub_vadd_mem c (hp₁ s₂ hs₂) (hp₂ s₂ hs₂) (hp₃ s₂ hs₂)
le_sSup := fun _ _ h => Set.Subset.trans (Set.subset_biUnion_of_mem h) (subset_spanPoints k _)
sSup_le := fun _ _ h => spanPoints_subset_coe_of_subset_coe (Set.iUnion₂_subset h)
sInf_le := fun _ _ => Set.biInter_subset_of_mem
le_inf := fun _ _ _ => Set.subset_inter }
