sep_infs_le — Mathlib

English

For sets S, T ⊆ α and a ∈ α, the a-cut of the inf-set S ⊼ T equals the infimum of the a-cuts: {b ∈ S ⊼ T | a ≤ b} = {b ∈ S | a ≤ b} ⊼ {b ∈ T | a ≤ b}.

Русский

Для множеств S, T ⊆ α и элемента a ∈ α верхняя граница a разреза инф-множества S ⊼ T равна инфимину моноcов a-границ: {b ∈ S ⊼ T | a ≤ b} = {b ∈ S | a ≤ b} ⊼ {b ∈ T | a ≤ b}.

LaTeX

$$$\\{ b \\in s \\⊼ t \\mid a \\le b \\} = \\{ b \\in s \\mid a \\le b \\} \\⊼ \\{ b \\in t \\mid a \\le b \\}$$$

Lean4

theorem sep_infs_le (s t : Set α) (a : α) : {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b} := by ext; aesop

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