filter_infs_le — Mathlib

English

With a decidable linear order, the filter of an infimum equals the infimum of filtered parts: {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}.

Русский

При допустимом линейном порядке фильтр от инфимума равен инфимума фильтрованных частей: {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}.

LaTeX

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

Lean4

theorem filter_infs_le [DecidableLE α] (s t : Finset α) (a : α) :
    {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b} := by
  simp only [← coe_inj, coe_filter, coe_infs, ← mem_coe, Set.sep_infs_le]

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