inr

Mathlib.Data.Finset.Lattice.Lemmas

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.inr

English

insert a s = {a} ∪ s.

Русский

insert a s = {a} ∪ s.

LaTeX

$$$\\mathrm{insert}\\ a\ \\, s = \\{a\\} \\cup s$$$

Lean4

@[aesop unsafe apply (rule_sets := [finsetNonempty])]
theorem inr {s t : Finset α} (h : t.Nonempty) : (s ∪ t).Nonempty :=
  h.mono subset_union_right

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

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

Разделы

Аффилиация

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