dom_of_mem_fix

Mathlib.Data.PFun

URI: https://scilib.ai/kg/mathlib#PFun.dom_of_mem_fix

← MathLib Explorer

English

If b ∈ f.fix a, then (f a).Dom holds.

Русский

Если b ∈ f.fix(a), то (f(a)).Dom верно.

LaTeX

$$$b \\in f.fix(a) \\Rightarrow (f(a)).\\mathrm{Dom}$$$

Lean4

theorem dom_of_mem_fix {f : α →. β ⊕ α} {a : α} {b : β} (h : b ∈ f.fix a) : (f a).Dom :=
  by
  let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
  rw [WellFounded.fixF_eq] at h₂; exact h₂.fst.fst

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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