Skip to content

Commit c800924

Browse files
authored
rename ciInf_le_inf to ciInf_inf_le
1 parent d5dcfef commit c800924

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ theorem ciSup_sup_le {f g : ι → α} : ⨆ x, f x ⊔ g x ≤ (⨆ x, f x) ⊔
387387
exact le_sup_right
388388
exact ciSup_sup_eq hf hg |>.le
389389

390-
theorem ciInf_le_inf {f g : ι → α} : (⨅ x, f x) ⊓ (⨅ x, g x) ≤ ⨅ x, f x ⊓ g x :=
390+
theorem ciInf_inf_le {f g : ι → α} : (⨅ x, f x) ⊓ (⨅ x, g x) ≤ ⨅ x, f x ⊓ g x :=
391391
ciSup_sup_le (α := αᵒᵈ)
392392

393393
/-- Indexed version of `exists_lt_of_lt_csSup`.

0 commit comments

Comments
 (0)