instNatCast

Mathlib.Algebra.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.instNatCast

English

Assuming a natural-number cast on α, NonemptyInterval α inherits a NatCast structure via natCast n = pure (Nat.cast n).

Русский

Пусть задан natCast на α; NonemptyInterval α получает структуру NatCast через natCast n = pure (Nat.cast n).

LaTeX

$$$\\text{NatCast}\\ (\\mathrm{NonemptyInterval}\\ \\alpha)$$$

Lean4

instance : NatCast (NonemptyInterval α) where natCast n := pure <| Nat.cast n

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

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

Разделы

Аффилиация

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