coind

Mathlib.Data.Subtype

URI: https://scilib.ai/kg/mathlib#Subtype.coind

Lean4

/-- Defining a map into a subtype, this can be seen as a "coinduction principle" of `Subtype` -/
@[simps]
def coind {α β} (f : α → β) {p : β → Prop} (h : ∀ a, p (f a)) : α → Subtype p := fun a ↦ ⟨f a, h a⟩

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

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

Разделы

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

Аффилиация

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