English
The Dep relation in the pullback is characterized by a disjunction: either image-dependent or independence with non-injective mapping.
Русский
Связь Dep в проекции обратно характеризуется либо зависимость образа, либо независимость при неинъективном отображении.
LaTeX
$$(N.comap f).Dep I \iff N.Dep (f'' I) \lor (N.Indep (f'' I) \land \neg InjOn f I)$$
Lean4
@[simp]
theorem comap_dep_iff : (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ (N.Indep (f '' I) ∧ ¬InjOn f I) :=
by
rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]
refine ⟨by grind, ?_⟩
rintro (⟨hI, hIE⟩ | hI)
· exact ⟨fun h ↦ (hI h).elim, hIE⟩
rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]
simpa using hI.1.subset_ground
