mem_of_subset — Mathlib

English

Let p be a SetLike element representing a subset of a base set B. If s is a subset of p (in the ambient Set B sense) and x is an element of s, then x is an element of p.

Русский

Пусть p представляет подмножество множества B через структуру SetLike. Если s ⊆ p и x ∈ s, то x ∈ p.

LaTeX

$$$ (s \subseteq p) \land (x \in s) \Rightarrow x \in p $$$

Lean4

@[aesop 5% (rule_sets := [SetLike!])]
theorem mem_of_subset {s : Set B} (hp : s ⊆ p) {x : B} (hx : x ∈ s) : x ∈ p :=
  hp hx

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