English
For a symmetric relation r and map f, fromRel(Relation.map_symmetric r f) equals the image of Sym2.fromRel hr under map f.
Русский
Для симметричного отношения r и отображения f выполняется равенство fromRel(Relation.map_symmetric r f) = Sym2.map f '' Sym2.fromRel r.
LaTeX
$$$$ \mathrm{fromRel}( \mathrm{Relation.map\_symmetric}(hr,f) ) = \mathrm{Sym2.map}\,f \;''\; \mathrm{Sym2.fromRel}(hr). $$$$
Lean4
theorem fromRel_relationMap {r : α → α → Prop} (hr : Symmetric r) (f : α → β) :
fromRel (Relation.map_symmetric hr f) = Sym2.map f '' Sym2.fromRel hr :=
by
ext ⟨a, b⟩
simp only [fromRel_proj_prop, Relation.Map, Set.mem_image, Sym2.exists, map_pair_eq, Sym2.eq, rel_iff', Prod.mk.injEq,
Prod.swap_prod_mk, and_or_left, exists_or, iff_self_or, forall_exists_index, and_imp]
exact fun c d hcd hc hd ↦ ⟨d, c, hr hcd, hd, hc⟩
