restrictPreimage_mk

Mathlib.Data.Set.Restrict

URI: https://scilib.ai/kg/mathlib#Set.restrictPreimage_mk

English

If a ∈ f⁻¹(t), then t.restrictPreimage f ⟨a, h⟩ = ⟨f(a), h⟩.

Русский

Если a принадлежит предобразу f⁻¹(t), то t.restrictPreimage f ⟨a,h⟩ равно ⟨f(a), h⟩.

LaTeX

$$$t.restrictPreimage f \; \langle a, h \rangle = \langle f(a), h \rangle$$$

Lean4

@[simp]
theorem restrictPreimage_mk (h : a ∈ f ⁻¹' t) : t.restrictPreimage f ⟨a, h⟩ = ⟨f a, h⟩ :=
  rfl

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

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

Разделы

Аффилиация

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