English
Same membership equivalence for insert lemmas; formalized as mem_insert equivalence.
Русский
Та же эквивалентность членства для лемм вставки; формализовано как mem_insert еквивалентность.
LaTeX
$$$ \\operatorname{mem}(\\mathrm{insert}\\ b\\ s\\, a) = \\operatorname{Or}(a=b, \\operatorname{mem}(s,a)) $$$
Lean4
theorem finset_inf_arrow_factors {I : Type*} {B : C} (s : Finset I) (P : I → Subobject B) (i : I) (m : i ∈ s) :
(P i).Factors (s.inf P).arrow := by
classical
revert i m
induction s using Finset.induction_on with
| empty => rintro _ ⟨⟩
| insert _ _ _ ih =>
intro _ m
rw [Finset.inf_insert]
simp only [Finset.mem_insert] at m
rcases m with (rfl | m)
· rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
exact factors_comp_arrow _
· rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
apply factors_of_factors_right
exact ih _ m
