English
In a distributive lattice, truncInf (s ∪ t) a equals truncInf s a ⊓ truncInf t a whenever a ∈ upperClosure s and a ∈ upperClosure t.
Русский
В распределительной решётке truncInf(s ∪ t) a = truncInf s a ⊓ truncInf t a, если a ∈ upperClosure s и a ∈ upperClosure t.
LaTeX
$$$a \in \operatorname{upperClosure}(s) \land a \in \operatorname{upperClosure}(t) \Rightarrow \operatorname{truncatedInf}(s \cup t) \, a = \operatorname{truncatedInf} s \, a \sqcap \operatorname{truncatedInf} t \, a$$$
Lean4
theorem map_truncatedInf (e : α ≃o β) (s : Finset α) (a : α) :
e (truncatedInf s a) = truncatedInf (s.map e.toEquiv.toEmbedding) (e a) :=
by
have : e a ∈ upperClosure (s.map e.toEquiv.toEmbedding) ↔ a ∈ upperClosure s := by simp
simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]
congr with h
simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv, OrderIso.le_iff_le, id,
inf'_map]
