covBy_insert — Mathlib

English

Let s be a subset and a an element not contained in s. Then s is immediately below insert a s in the inclusion order: s is strictly contained in insert a s, and there is no subset strictly between them.

Русский

Пусть s — подмножество, а a — элемент, не входящий в s. Тогда s находится непосредственно ниже insert a s в порядке включения: s ⊊ insert a s и между ними нет другого множества.

LaTeX

$$$ s \covBy \operatorname{insert}(a,s) $$$

Lean4

@[simp]
theorem covBy_insert (ha : a ∉ s) : s ⋖ insert a s :=
  (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha

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