assump

Mathlib.Tactic.Linarith.Oracle.FourierMotzkin

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.PComp.assump

Lean4

/-- `PComp.assump c n` creates a `PComp` whose comparison is `c` and whose source is
`CompSource.assump n`, that is, `c` is derived from the `n`th hypothesis.
The history is the singleton set `{n}`.
No variables have been eliminated (effectively or implicitly).
-/
def assump (c : Comp) (n : ℕ) : PComp where
  c := c
  src := CompSource.assump n
  history := { n }
  effective := .empty
  implicit := .empty
  vars := .ofList c.vars _

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

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

Разделы

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

Аффилиация

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