strictMono_extent — Mathlib

English

Extent is strictly monotone with respect to the concept order: if c < d, then c.extent ⊂ d.extent.

Русский

Экстент строго монотонен относительно порядка концептов: если c < d, то c.extent ⊂ d.extent.

LaTeX

$$$\forall c,d : \mathrm{Concept}\,\alpha\,\beta\,r,\; c < d \rightarrow c.extent \subset d.extent$$$

Lean4

theorem strictMono_extent : StrictMono (@extent α β r) := fun _ _ => extent_ssubset_extent_iff.2

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