mapEmbedding_isLoop_iff — Mathlib

English

For an embedding f, the IsLoop status of the mapped element equals the IsLoop status of the original element.

Русский

Для вложения f, статус IsLoop переданного элемента равен статусу IsLoop исходного элемента.

LaTeX

$$$ (M.mapEmbedding f).IsLoop (f e) \iff M.IsLoop e $$$

Lean4

@[simp]
theorem mapEmbedding_isLoop_iff {f : α ↪ β} : (M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e := by
  simp [mapEmbedding, isLoop_iff, isLoop_iff, map_closure_eq, preimage_empty, ← closure_empty]

Похожие утверждения