English
A variant of directedness for partialSections, establishing the same inclusion property in a slightly simplified form.
Русский
Вариант направленности для partialSections, устанавливающий то же свойство включения в слегка упрощённой форме.
LaTeX
$$$ \text{Directed }\mathrm{partialSections} :\forall A,B, \mathrm{partialSections}(F,A) \subseteq \mathrm{partialSections}(F,A\sqcup B) \text{ и } \mathrm{partialSections}(F,B) \subseteq \mathrm{partialSections}(F,A\sqcup B) $$$
Lean4
theorem directed : Directed Superset fun G : FiniteDiagram J => partialSections F G.2 := by
classical
intro A B
let ιA : FiniteDiagramArrow A.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
⟨f.1, f.2.1, Finset.mem_union_left _ f.2.2.1, Finset.mem_union_left _ f.2.2.2.1, f.2.2.2.2⟩
let ιB : FiniteDiagramArrow B.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
⟨f.1, f.2.1, Finset.mem_union_right _ f.2.2.1, Finset.mem_union_right _ f.2.2.2.1, f.2.2.2.2⟩
refine ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, ?_, ?_⟩
· rintro u hu f hf
have : ιA f ∈ A.2.image ιA ⊔ B.2.image ιB :=
by
apply Finset.mem_union_left
rw [Finset.mem_image]
exact ⟨f, hf, rfl⟩
exact hu this
· rintro u hu f hf
have : ιB f ∈ A.2.image ιA ⊔ B.2.image ιB :=
by
apply Finset.mem_union_right
rw [Finset.mem_image]
exact ⟨f, hf, rfl⟩
exact hu this
