mem_of_mem_of_subset

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.mem_of_mem_of_subset

English

If x ∈ s and s ⊆ t, then x ∈ t.

Русский

Если x ∈ s и s ⊆ t, то x ∈ t.

LaTeX

$$$x \in s \rightarrow (s \subseteq t) \rightarrow x \in t$$$

Lean4

@[trans]
theorem mem_of_mem_of_subset {x : α} {s t : Set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t :=
  h hx

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

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

Разделы

Аффилиация

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