English
Another instance asserting nonemptiness of a StructuredArrow for walking reflexive pair objects.
Русский
Еще один пример непустоты структурированной стрелки для объектов WalkingReflexivePair.
LaTeX
$$$\forall X:\text{WalkingReflexivePair},\; \operatorname{Nonempty}(\mathrm{StructuredArrow}(X,\ \text{inclusionWalkingReflexivePair}))$$$
Lean4
instance (X : WalkingReflexivePair) : IsConnected (StructuredArrow X inclusionWalkingReflexivePair) := by
cases X with
| zero =>
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
· exact (h₂ (StructuredArrow.homMk .left)).2 h₁
· exact h₁
| one =>
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _)) (fun p h₁ h₂ ↦ ?_)
have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
· exact (h₂ (StructuredArrow.homMk .left)).2 hₗ
· exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ
all_goals assumption
