target_subset_range

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.target_subset_range

English

The target of a partial equivalence is contained in the range of its forward map.

Русский

Целевая область частичного эквивалента содержится в образе отображения.

LaTeX

$$$e. target \subseteq \mathrm{range}(e.toFun)$$$

Lean4

theorem target_subset_range : e.target ⊆ range e := fun x hx ↦ ⟨e.symm x, right_inv e hx⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru