isSemilinearSet — Mathlib

English

If s is a proper linear set, then s is a semilinear set.

Русский

Если s — правильное линейное множество, то оно является семилинейным множеством.

LaTeX

$$$IsProperLinearSet(s) \Rightarrow IsProperSemilinearSet(s)$$$

Lean4

theorem isSemilinearSet (hs : IsProperSemilinearSet s) : IsSemilinearSet s :=
  by
  rcases hs with ⟨S, hS, hS', rfl⟩
  exact ⟨S, hS, fun s hs => (hS' s hs).isLinearSet, rfl⟩

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